#AI4Math

Shaping the future of mathematics in the age of AI. ~ Johan Commelin, Mateja Jamnik, Rodrigo Ochigame, Lenny Taelman, Akshay Venkatesh. www.math.ias.edu/~akshay/mnot... #AI4Math #LeanProver #ITP

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

LeanTutor: A Formally-Verified AI Tutor for Mathematical Proofs We present LeanTutor, a Large Language Model (LLM)-based tutoring system for math proofs. LeanTutor interacts with the student in natural language, formally verifies student-written math proofs in Lea...

LeanTutor: A formally-verified AI tutor for mathematical proofs. ~ Manooshree Patel, Rayna Bhattacharyya, Thomas Lu, Arnav Mehta, Niels Voss, Narges Norouzi, Gireeja Ranade. arxiv.org/abs/2506.083... #LeanProver #ITP #Math #AI4Math

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

Formalizing a proof in Lean using Claude Code YouTube video by Terence Tao

Formalizing a proof in Lean using Claude Code. ~ Terence Tao. youtu.be/JHEO7cplfk8 #LeanProver #ITP #AI4Math

3 0 1 0

José A. Alonso

@jalonso.eurosky.social

1 week ago

Readings shared March 4, 2026 The readings shared in Bluesky on 4 March 2026 are: When AI writes the world’s software, who verifies it? ~ Leonardo de Moura. #AI #LeanProver #ITP Formalising sphere packing in Lean. ~ Chris Birkbec

Readings shared March 04, 2026. jaalonso.github.io/vestigium/po... #AI #AI4Math #CoqProver #FunctionalProgramming #Haskell #ITP #LeanProver #Math #RocqProver

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 week ago

The Purpose of Proofs In discussions of AI and Mathematics, the discussion often goes to mathematical proofs, such as the the First Proof challenge. So let's lo...

The purpose of proofs. ~ Lance Fortnow. blog.computationalcomplexity.org/2026/03/the-... #LeanProver #ITP #AI4Math

4 1 0 0

José A. Alonso

@jalonso.eurosky.social

1 week ago

Completing the formal proof of higher-dimensional sphere packing — Math, Inc. Dedicated to verified superintelligence via autoformalization.

Completing the formal proof of higher-dimensional sphere packing. www.math.inc/sphere-packing #LeanProver #ITP #AI4Math

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 week ago

Reseña de «Completing the formal proof of higher-dimensional sphere pa Hoy se ha publicado el anuncio de la formalización total de los teoremas de Maryna Viazovska sobre el empaquetamiento de esferas. Con una extensión de aproximadamente 200,000 líneas de código en el le

Reseña de «Completing the formal proof of higher-dimensional sphere packing». jaalonso.github.io/vestigium/po... #AI4Math

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

2 weeks ago

Reseña de «AI that can prove it’s right: Verification as the missing l En el vídeo «AI that can prove it’s right: Verification as the missing layer in AI», Carina Hong explica cómo Axiom Math está desarrollando una inteligencia artificial matemática capaz de autoverifica

Reseña de «AI that can prove it’s right: Verification as the missing layer in AI». jaalonso.github.io/vestigium/po... #AI4Math #LeanProver

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

2 weeks ago

Readings shared February 24, 2026 The readings shared in Bluesky on 24 February 2026 are: Formalizing Gröbner basis theory in Lean. ~ Junyu Guo, Hao Shen, Junqi Liu, Lihong Zhi. #LeanProver #ITP #Math Integral curves and flows on Ban

Readings shared February 24, 2026. jaalonso.github.io/vestigium/po... #AI4Math #ATP #Agda #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Reasoning #Vampire

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

2 weeks ago

M2F: Automated Formalization of Mathematical Literature at Scale Automated formalization of mathematics enables mechanical verification but remains limited to isolated theorems and short snippets. Scaling to textbooks and research papers is largely unaddressed, as ...

M2F: Automated formalization of mathematical literature at scale. ~ Zichen Wang et als. arxiv.org/abs/2602.170... #AI4Math #ITP #LeanProver

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

2 weeks ago

Math in the Age of AI | Communications of the ACM You will be notified whenever a record that you have chosen has been cited.

Math in the age of AI. ~ Allyn Jackson. dl.acm.org/doi/full/10.... #AI4Math

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

3 weeks ago

Readings shared February 19, 2026 The readings shared in Bluesky on 19 February 2026 are: Hennessy-Milner logic in CSLib, the Lean computer science library. ~ Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker. #LeanProver #ITP

Readings shared February 19, 2026. jaalonso.github.io/vestigium/po... #AI4Math #ATP #CSLib #CompSci #Dedukti #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Mizar #RocqProver #Vampire

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

3 weeks ago

Proof Assistants in the Age of AI Leonardo de Moura — Creator of Lean and Z3

Proof assistants in the age of AI. ~ Leonardo de Moura. leodemoura.github.io/blog/2026/02... #AI4Math #ITP

3 0 0 0

José A. Alonso

@jalonso.eurosky.social

3 weeks ago

Mathematics and Machine Creativity: A Survey on Bridging Mathematics with AI This paper presents a comprehensive survey on the applications of artificial intelligence (AI) in mathematical research, highlighting the transformative role AI has begun to play in this domain. Tradi...

Mathematics and machine creativity: A Survey on bridging mathematics with AI. ~ Shizhe Liang, Wei Zhang, Tianyang Zhong. arxiv.org/abs/2412.165... #AI4Math #ITP

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

3 weeks ago

Reseña de «Machine assistance and the future of research mathematics» En el artículo «Mathematics and machine creativity: A survey on bridging mathematics with AI», se analiza cómo la IA transforma la investigación matemática. Aunque los modelos actuales fallan en lógic

Reseña de «Machine assistance and the future of research mathematics». jaalonso.github.io/vestigium/po... #AI4Math

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 month ago

Readings shared February 14, 2026 The readings shared in Bluesky on 14 February 2026 are: Formalization of the Golay-Hopf machine: A unified algebraic framework for Hida, Iwasawa, and Yang-Baxter structures. ~ Yoshihiro Hasegawa. #IT

Readings shared February 14, 2026. jaalonso.github.io/vestigium/po... #AI4Math #Agda #Clojure #CoqProver #FunctionalProgramming #Haskell #ITP #LeanProver #Lisp #Logic #Math #Minlog #Prolog #RustLang

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 month ago

LLMs for math research. ~ Dmitry Rybin. drive.google.com/drive/folder... #AI4Math #ITP #LeanProver

2 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 month ago

To be a frog with wings, should you choose (Recent progress on AI for mathematics and how to get involved). ~ Kevin Barreto. drive.google.com/file/d/1VQk1... #AI4Math #ITP #LeanProver

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 month ago

Towards Autonomous Mathematics Research Recent advances in foundational models have yielded reasoning systems capable of achieving a gold-medal standard at the International Mathematical Olympiad. The transition from competition-level probl...

Towards autonomous mathematics research. ~ Tony Feng et als. arxiv.org/abs/2602.101... #AI4Math

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

1 month ago