#aiformath — Public Fediverse posts

MIT researchers just snagged 'AI for Math' grants to turbocharge mathematical discovery! They're bridging the gap between massive databases like LMFDB and formal proof systems such as Lean's Mathlib. This isn't just about faster calcs; it's about making unformalized knowledge accessible to AI for new breakthroughs.

#AIforMath #Mathematics #TechNews #Research #LLMs
https://news.mit.edu/2025/ai-for-math-grants-accelerate-mathematical-discovery-0922

Will AI make us better mathematicians, or just better at validating AI's math?

Readings shared June 19, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/20-readings_shared_06-19-25 #AI #AIforMath #CoqProver #ITP #IsabelleHOL #LLMs #LeanProver #Math #Rocq

Reviving DSP for advanced theorem proving in the era of reasoning models. ~ Chenrui Cao, Liangcheng Song, Zenan Li, Xinyi Le, Xian Zhang, Hui Xue, Fan Yang. https://arxiv.org/abs/2506.11487v1 #AI #Math #AIforMath #LLMs #ITP #LeanProver

Reseña de «Can A.I. quicken the pace of math discovery?». https://jaalonso.github.io/vestigium/posts/2025/06/19-can-ai-quicken-the-pace-of-math-discovery/ #AI #Math #AIforMath #ITP #LeanProver

Readings shared June 15, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/16-readings_shared_06-15-25 #AI #AIforMath #CoqProver #FunctionalProgramming #Haskell #ITP #LeanProver #Lisp #Math #Programming #Rocq

Reseña de «Hardest problems in mathematics, physics & the future of AI». https://jaalonso.github.io/vestigium/posts/2025/06/15-hardest-problems-in-mathematics-physics-the-future-of-ai/ #ITP #LeanProver #AI #Math #AIforMath

Readings shared June 13, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/14-readings_shared_06-13-25 #AI #AIforMath #Autoformalization #CoqProver #HOL_Light #ITP #IsabelleHOL #LLMs #LeanProver #Logic #MLLMs #Math #Rocq

The abc conjecture almost always — autoformalized. ~ Jesse Michael Han et als. https://github.com/morph-labs/lean-abc-true-almost-always #Autoformalization #AIforMath #ITP #LeanProver

Trinity: an autoformalization system for verified superintelligence. https://www.morph.so/blog/trinity #Autoformalization #AIforMath #ITP #LeanProver

Reseña de «Mathesis: Towards formal theorem proving from natural languages». https://jaalonso.github.io/vestigium/posts/2025/06/13-resena-de-mathesis-towards-formal-theorem-proving-from-natural-languages/ #AI #LLMs #Math #ITP #LeanProver #AIforMath

Mathesis: Towards formal theorem proving from natural languages. ~ Yu Xuejun et als. https://arxiv.org/abs/2506.07047 #AI #LLMs #Math #ITP #LeanProver #AIforMath

Reseña de «MATP-BENCH: Can MLLM be a good automated theorem prover for multimodal problems?». https://jaalonso.github.io/vestigium/posts/2025/06/13-resena-de-matp-bench-can-mllm-be-a-good-automated-theorem-prover-for-multimodal-problems/ #AI #MLLMs #Math #ITP #IsabelleHOL #LeanProver #CoqProver #AIforMath

MATP-BENCH: Can MLLM be a good automated theorem prover for multimodal problems? ~ Zhitao He et als. https://arxiv.org/abs/2506.06034 #AI #MLLMs #Math #ITP #IsabelleHOL #LeanProver #CoqProver #AIforMath

StepProof: Step-by-step verification of natural language mathematical proofs. ~ Xiaolin Hu, Qinghua Zhou, Bogdan Grechuk, Ivan Y. Tyukin. https://arxiv.org/abs/2506.10558 #LLMs #ITP #IsabelleHOL #Math #AIforMath

Readings shared June 11, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/12-readings_shared_06-11-25 #AIforMath #CompSci #IA #ITP #LeanProver #Logic #Math #RustLang #SMT #Z3

Reseña de 'LeanTutor: A formally-verified AI tutor for mathematical proofs'. https://jaalonso.github.io/vestigium/posts/2025/06/11-resena-de-leantutor-a-formally-verified-ai-tutor-for-mathematical-proofs/ #ITP #LeanProver #Math #AIforMath #Teaching

LeanTutor: A formally-verified AI tutor for mathematical proofs. ~ Manooshree Patel et als. https://arxiv.org/abs/2506.08321 #ITP #LeanProver #Math #AIforMath #Teaching

El futuro del razonamiento matemático: Integrando IA y Lean. https://jaalonso.github.io/vestigium/posts/2025/06/11-el-futuro-del-razonamiento-matematico-integrando-ia-y-lean/ #IA #ITP #LeanProver #Math #AIforMath

Readings shared June 10, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/11-readings_shared_06-10-25 #AI #AIforMath #ATP #AlphaProof #Emacs #ITP #IsabelleHOL #LLMs #LeanProver #Math #Prover9

El proyecto ETP (Un caso de estudio en investigación matemática colaborativa y formalizada). https://jaalonso.github.io/vestigium/posts/2025/06/10-el-proyecto-etp-un-caso-de-estudio-en-investigacion-matematica-colaborativa-y-formalizada/ #AIforMath #ITP #LeanProver #Math

The equational theories project: advancing collaborative mathematical research at scale. ~ Terence Tao et als. https://terrytao.wordpress.com/wp-content/uploads/2025/06/math-experiments.pdf #ITP #LeanProver #Math #AIforMath

El futuro de las matemáticas: Descubrimiento colaborativo entre humanos y máquinas. https://jaalonso.github.io/vestigium/posts/2025/06/10-el-futuro-de-las-matematicas-descubrimiento-colaborativo-entre-humanos-y-maquinas/ #AIforMath #AI #Math

AI for Math: The future of collaborative discovery. ~ Mateja Jamnik. https://www.youtube.com/live/WdXnMrT1X_k #AIforMath

AlphaProof - Aprendizaje por refuerzo aplicado a la demostración matemática. https://jaalonso.github.io/vestigium/posts/2025/06/10-alphaproof-aprendizaje-por-refuerzo-aplicado-a-la-demostracion-matematica/ #AI #Math #AIforMath #ITP #LeanProver #AlphaProof

AlphaProof: When RL meets formal maths. ~ Thomas Hubert. https://www.youtube.com/live/xZIqn4V6O0A #AI #Math #AIforMath #ITP #LeanProver #AlphaProof

New AI stuns mathematicians with its problem-solving skill. ~ David H Bailey. https://mathscholar.org/2025/06/new-ai-stuns-mathematicians-with-its-problem-solving-skill/ #AI #LLMs #Math #AIforMath #ITP #LeanProver

Readings shared June 9, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/09-readings_shared_06-09-25 #AI #AIforMath #CategoryTheory #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #LogicProgramming #Math #Prolog #Rust

Evaluando la IA con problemas matemáticos inéditos de nivel experto. https://jaalonso.github.io/vestigium/posts/2025/06/09-evaluando-la-ia-con-problemas-matematicos-ineditos-de-nivel-experto/ #AIforMath #AI #LLMs #Math

At secret math meeting, researchers struggle to outsmart AI (The world's leading mathematicians were stunned by how adept artificial intelligence is at doing their jobs). ~ Lyndie Chiou. https://www.scientificamerican.com/article/inside-the-secret-meeting-where-mathematicians-struggled-to-outsmart-ai/ #AIforMath #AI #LLMs #Math