#AI4Math hashtag - Bluesky

@jalonso.eurosky.social

12 hours ago

Embracing AI and formalization: Experimenting with tomorrow’s mathematical tools. ~ Jarod Alper. pubs.ams.org/BULL/0000-00... #AI4Math #LeanProver #ITP #Math

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

13 hours ago

Autoformalization: A year of progress. ~ Auguste Poiroux. tube.switch.ch/videos/NVLp5... #AI4Math #LeanProver

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

14 hours ago

Mathematics in the library of Babel. ~ Daniel Litt. www.daniellitt.com/blog/2026/2/... #AI4Math

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

14 hours ago

As AI keeps improving, mathematicians struggle to foretell their own future First Proof is an effort to see whether LLMs can contribute meaningfully to pure mathematics research. The dust has settled on round one, and the results are surprising

As AI keeps improving, mathematicians struggle to foretell their own future. ~ Joseph Howlett. www.scientificamerican.com/article/as-a... #AI4Math #LeanProver

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

14 hours ago

What happens when AI starts checking mathematicians’ work A start-up has surprised the scientific community with a breakthrough: translating a modern proof into a programming language for verification using AI. But not everyone is celebrating

What happens when AI starts checking mathematicians’ work. ~ Manon Bischoff. www.scientificamerican.com/article/what... #AI4Math #LeanProver

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

14 hours ago

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

4 days ago

Readings shared March 24, 2026 The readings shared in Bluesky on 24 March 2026 are: Synthetic differential geometry in Lean. ~ Riccardo Brasca, Gabriella Clemente. #LeanProver #ITP #Math The spectral comb and the Riemann hypothesi

Readings shared March 24, 2026. jaalonso.github.io/vestigium/po... #AI4Math #Autoformalization #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Math

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

5 days ago

OpenGauss: an open source, state of the art autoformalization harness — Math, Inc. OpenGauss is a state-of-the-art open-source autoformalization harness for Lean, built for practical proof engineering workflows.

OpenGauss: an open source, state of the art autoformalization harness. www.math.inc/opengauss #AI4Math #LeanProver #ITP #Autoformalization

3 0 0 0

José A. Alonso

@jalonso.eurosky.social

2 weeks ago

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

2 0 0 0

José A. Alonso

@jalonso.eurosky.social

2 weeks ago

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

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

2 weeks ago

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

1 1 0 0

José A. Alonso

@jalonso.eurosky.social

2 weeks ago

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

2 0 0 0

Mark Pors 🦖

@pors.bsky.social

2 weeks ago

This paper showed up in my Paperzilla #AI4Math feed:

paperzilla.ai/digest/0fbbf...

0 0 1 0

José A. Alonso

@jalonso.eurosky.social

2 weeks ago

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

0 0 0 0

José A. Alonso

@jalonso.eurosky.social

2 weeks ago

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

1 0 0 0

José A. Alonso

@jalonso.eurosky.social

2 weeks 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

2 weeks 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

3 weeks 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

3 weeks 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

3 weeks 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

3 weeks 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

1 month 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

1 month 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

1 month 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

1 month 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

1 month 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

1 month 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

1 month 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

1 month 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