#AI4Math
LightNews LightNews
jalonso.eurosky.social
The mathematical sciences in an AI-enabled World (Opportunities, risks and community needs). ~ Christoph Reisinger, Rachel Bearon, Thomas Bloom, Jennifer Gaskell, David Leslie, Zubin Siganporia.

www.acadmathsci.org.uk/wp-content/u...

#AI4Math
November 1, 2026 at 11:17 AM
jalonso.eurosky.social
Math 2.0. — Terence Tao.

youtu.be/aHpPoNNTOKY

#AI4Math
Terence Tao: Math 2.0
YouTube video by SAIR
youtu.be
November 3, 2026 at 12:01 PM
jalonso.eurosky.social
AI reviews are the new normal. ~ Tim Gehrunger.

proofsandprompts.com/2026/10/31/a...

#AI4Math
AI reviews are the new normal
The mathematical literature contains mistakes. Articles on the arXiv are not refereed, and even peer review does not guarantee that articles are error-free. In private communication, many (tenured …
proofsandprompts.com
November 1, 2026 at 12:16 PM
markriedl.bsky.social
Georgia Tech just launched a new Center for Computer Algebra and AI for Math sites.gatech.edu/ai4math-cent...
October 27, 2026 at 2:31 AM
jalonso.eurosky.social
Mathematicians in the time of AI. — Yu Deng.

youtu.be/fIjT6d5c19E

#AI4Math
Yu Deng: Mathematicians in the time of AI
YouTube video by SAIR
youtu.be
November 3, 2026 at 11:58 AM
jalonso.eurosky.social
Report of "Summit on math research in the age of AI".

cmsa.fas.harvard.edu/media/2026/1...

#AI4Math
October 31, 2026 at 12:03 PM
jalonso.eurosky.social
Mathematics has changed. Let’s act like it. ~ Frank Calegari.

terrytao.wordpress.com/2026/11/01/m...

#AI4Math
Mathematics has changed. Let’s act like it
[This is a guest post by Frank Calegari. This blog post was initially written in a different file format and converted using AI. — T.] Why we should not be sad The release by OpenAI on Octobe…
terrytao.wordpress.com
November 3, 2026 at 11:45 AM
jalonso.eurosky.social
AI is shaking up math. But can its proofs be trusted?. ~ Celina Zhao.

www.science.org/content/arti...

#AI4Math
AI is shaking up math. But can its proofs be trusted?
As AI firms churn out math breakthroughs, researchers question use of Lean software as proof checker
www.science.org
October 31, 2026 at 12:20 PM
jalonso.eurosky.social
Egoless mathematics in the AI era. — Karthik C. S., Amit Sahai, Jie Xue.

terrytao.wordpress.com/2026/11/02/e...

#AI4Math
Egoless Mathematics in the AI Era
[This is a guest post by Karthik C. S., Amit Sahai, and Jie Xue. This blog post was initially written in a different file format and converted using AI. — T.] This is a good time for mathemat…
terrytao.wordpress.com
November 3, 2026 at 12:11 PM
jalonso.eurosky.social
Let’s stop writing papers… ~ Patrick Morris.

proofsandprompts.com/2026/10/30/l...

#AI4Math
Let’s stop writing papers…
In this essay, I put forward some ideas on what the future of mathematical culture could look like as well as thoughts and concrete suggestions for how we get there. My focus is centred around a mo…
proofsandprompts.com
October 31, 2026 at 12:11 PM
jalonso.eurosky.social
What does AI do for olympiad students? — Beckett Bradford.

proofsandprompts.com/2026/11/02/w...

#AI4Math
What Does AI Do for Olympiad Students?
“There’s a solid argument that AI has solved the IMO, in terms of being able to output LaTeX that would score a 7 on most or all of the questions, virtually guaranteeing highest honors there …
proofsandprompts.com
November 3, 2026 at 11:35 AM
jalonso.eurosky.social
KAPPA: Checking the proofs in statistics papers with Lean 4 and language model agents. ~ Zihua She, Xiao Wang.

arxiv.org/abs/2610.35596

#LeanProver #ITP #AI4Math
KAPPA: Checking the Proofs in Statistics Papers with Lean 4 and Language Model Agents
Papers in statistical theory rest on long proofs that few readers check line by line. We present KAPPA (Kit of Agents for Proof-checking Papers with a proof Assistant), open-source software that organ...
arxiv.org
November 2, 2026 at 12:57 PM
jalonso.eurosky.social
First Proof: A nuanced assessment of AI's ability to solve math problems. ~ Lauren Williams.

youtu.be/4RDv_g2NFf0

#AI4Math
First Proof: A Nuanced Assessment of AI's Ability to Solve Math Problems
YouTube video by Harvard Mathematics Department
youtu.be
October 29, 2026 at 10:28 AM
jalonso.eurosky.social
Weekly reads: Oct 26 – Nov 1, 2026. Also in Spanish on the blog.

jaalonso.github.io/vestigium/en...

#AI #AI4Math #Autoformalization #IsabelleHOL #ITP #Lean4Challenge #LeanProver #Logic #Math
Weekly reads: Oct 26 – Nov 1, 2026
Here are the 27 reads I shared on Mastodon this past week. This week's main thread is, once again, the future of mathematics in the age of AI, now with two community reports: "The mathematical science
jaalonso.github.io
November 2, 2026 at 8:07 AM
jalonso.eurosky.social
AI, mathematics, education, and a public goods problem. ~ Gireeja Ranade.

terrytao.wordpress.com/2026/10/29/a...

#AI4Math
AI, Mathematics, Education, and a public goods problem
[This is a guest post by Gireeja Ranade. This blog post was initially written in a different file format and converted using AI. — T.] The day after the Navier-Stokes result was announced, a …
terrytao.wordpress.com
October 31, 2026 at 12:15 PM
jalonso.eurosky.social
Weekly reads: Oct 19 – Oct 25, 2026.

🇬🇧 English: jaalonso.github.io/vestigium/en...

🇪🇸 Spanish: jaalonso.github.io/vestigium/po...

#AI #AI4Math #ITP #Lean4Challenge #LeanProver #Logic #LogicProgramming #Math #Prolog #RetoLean4
Weekly reads: Oct 19 – Oct 25, 2026
Here are the 42 reads I shared on Mastodon this past week. This week's main thread is, once again, the future of mathematics in the age of AI. Most of the AI4Math reads come from the Proofs and Prompt
jaalonso.github.io
October 26, 2026 at 7:28 AM
jalonso.eurosky.social
The classification of finite simple groups, formalized in Lean.

cfsg.axiommath.ai

#LeanProver #ITP #AI4Math #AI #Math
The Classification of Finite Simple Groups, formalized in Lean
A complete formalization in Lean of the first-generation proof of the classification of finite simple groups, with every logical step checked by Lean’s kernel.
cfsg.axiommath.ai
October 27, 2026 at 6:07 PM
jalonso.eurosky.social
Formalizing the Enormous Theorem (Axiom has formalized in Lean the classification of finite simple groups, the longest proof in the history of mathematics).

axiommath.ai/research/the...

#LeanProver #ITP #AI4Math #AI #Math
Formalizing the Enormous Theorem
Axiom has formalized in Lean the classification of finite simple groups, the longest proof in the history of mathematics.
axiommath.ai
October 27, 2026 at 5:00 PM
jalonso.eurosky.social
PaperFormalizer: Author-in-the-loop autoformalization of research papers in Lean. ~ Jiyuan Tan, Vasilis Syrgkanis, Jose Blanchet.

arxiv.org/abs/2610.31810

#LeanProver #ITP #AI4Math #Autoformalization
PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean
Even a carefully proofread paper can leave small gaps in its proofs or its stated assumptions. We introduce PaperFormalizer, a Lean-based agentic pipeline that helps authors find and close such gaps i...
arxiv.org
October 26, 2026 at 11:41 AM
jalonso.eurosky.social
Could AI help correct the mathematical literature? ~ Alonso Castillo-Ramirez.

proofsandprompts.com/2026/10/25/c...

#AI4Math
Could AI help correct the mathematical literature?
“We mathematicians know that published papers and books often contain mistakes: sometimes small, like a missing hypothesis or a wrong constant, and sometimes more serious, like a theorem that is fa…
proofsandprompts.com
October 26, 2026 at 11:50 AM
jalonso.eurosky.social
Disgusted by AI? ~ Marcus Zibrowius. proofsandprompts.com/2026/10/23/d...

#AI4Math
Disgusted by AI?
I completely disagree with the notion that AI companies have hijacked our mathematical culture and turned it into something new and unrecognizable. They have just taken our existing culture to its …
proofsandprompts.com
October 23, 2026 at 11:57 AM
jalonso.eurosky.social
AI and mathematics: public good, credit, and education. ~ András Juhász. proofsandprompts.com/2026/10/24/a...

#AI4Math #AI #Math
AI and Mathematics: Public Good, Credit, and Education
We should preserve the human ability to understand and explore mathematics, not preserve unsolved problems merely to protect a familiar way of working. The goal should be to enlarge public mathemat…
proofsandprompts.com
October 25, 2026 at 9:48 AM
jalonso.eurosky.social
Review of «Disgusted by AI?».

🇬🇧 English: jaalonso.github.io/vestigium/en...

🇪🇸 Spanish: jaalonso.github.io/vestigium/po...

#AI4Math
Review of «Disgusted by AI?»
In the article Disgusted by AI?, Marcus Zibrowius examines the resistance that much of the mathematical community feels toward the sudden arrival of AI. Initially, this rejection appears to be driven
jaalonso.github.io
October 23, 2026 at 2:14 PM
jalonso.eurosky.social
Review of «Towards a world mathematical commons».

🇬🇧 English: jaalonso.github.io/vestigium/en...

🇪🇸 Spanish: jaalonso.github.io/vestigium/po...

#AI4Math #LeanProver #ITP #AI #Math
Review of «Towards a world mathematical commons»
In his article «Towards a world mathematical commons», Kunal Marwaha observes that mathematics is a deeply creative and emotional pursuit that has outgrown individual mastery. As machines increasingly
jaalonso.github.io
October 23, 2026 at 3:39 PM
jalonso.eurosky.social
Mathematics of the future. Pavel Etingof et al. proofsandprompts.com/2026/10/21/m...

#AI4Math
Mathematics of the Future
“Rapid advances in AI are transforming research, and for the growth of mathematical knowledge, this is thrilling. For our profession, however, this raises critical questions: Will there be a role f…
proofsandprompts.com
October 22, 2026 at 11:51 AM