Reseña de «Mathematicians in the age of AI» En el artículo «Mathematicians in the age of AI», Jeremy Avigad describe cómo la evolución de la IA ha sido meteórica desde la aparición de la IA generativa a finales de 2022, cuando sus capacidades m

Reseña de «Mathematicians in the age of AI». jaalonso.github.io/vestigium/po... #AI4Math

Reseña de «AI for mathematical and scientific discovery» En el vídeo «AI for mathematical and scientific discovery», se explica cómo la IA ha evolucionado desde resolver problemas escolares hasta alcanzar niveles de medalla de oro en olimpiadas matemáticas.

Reseña de «AI for mathematical and scientific discovery». jaalonso.github.io/vestigium/po... #AI4Math

Reseña de «Shaping the future of mathematics in the age of AI» En el artículo «Shaping the future of mathematics in the age of AI», coescrito por el medalla Fields Akshay Venkatesh, se analiza cómo la IA transforma la disciplina. Destacan métodos simbólicos como

Reseña de «Shaping the future of mathematics in the age of AI». jaalonso.github.io/vestigium/po... #AI4Math

Readings shared March 9, 2026 The readings shared in Bluesky on 9 March 2026 are: Fantastic simprocs and how to write them. ~ Yaël Dillies, Paul Lezeau. #LeanProver #ITP Formalization in Lean of faithfully flat descent of project

Readings shared March 09, 2026. jaalonso.github.io/vestigium/po... #AI #AI4Math #CategoryTheory #CoqProver #Emacs #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LambdaCalculus #LeanProver #Lisp #Math #Physics #RocqProver

This paper showed up in my Paperzilla #AI4Math feed:

paperzilla.ai/digest/0fbbf...

Mathematicians in the age of AI Recent developments show that AI can prove research-level theorems in mathematics, both formally and informally. This essay urges mathematicians to stay up-to-date with the technology, to consider the...

Mathematicians in the age of AI. ~ Jeremy Avigad. arxiv.org/abs/2603.03684 #AI4Math #LeanProver #ITP

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Gemini Deep Think: Redefining the Future of Scientific Research Gemini Deep Think is accelerating discovery in maths, physics, and computer science by acting as a powerful scientific companion for researchers.

Accelerating mathematical and scientific discovery with Gemini Deep Think. ~ Thang Luong and Vahab Mirrokni. deepmind.google/blog/acceler... #AI4Math

Leaning on AI. ~ Rado Kirov. rkirov.github.io/posts/lean5/ #LeanProver #ITP #AI4Math

Reseña de «Machine assistance and the future of research mathematics» Ayer se publicó la conferencia de Terence Tao titulada «Machine assistance and the future of research mathematics», donde analiza la transformación de esta disciplina por la IA. Tao señala que las mat

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

Readings shared February 4, 2026 The readings shared in Bluesky on 4 February 2026 are: "Five-Point Haskell": Total depravity (and defensive typing). ~ Justin Le. #Haskell #FunctionalProgramming 'Sets' revisited: Working with a larg

Readings shared February 09, 2026. jaalonso.github.io/vestigium/po... #AI4Math #CompSci #ITP #LeanProver #Math

Accelerating mathematics Let’s say that someone had a big pot of money, and wanted to use it to accelerate mathematical discovery. How might they go about doing this? The traditional approach Historically it has been…

Accelerating mathematics. ~ Kevin Buzzard. xenaproject.wordpress.com/2026/02/09/a... #AI4Math #ITP #LeanProver