Congratulations!!

I am honored to be part of the #guggfellows2025 class. My Guggenheim project is on AI systems that can discover new math in an open-ended way. Many thanks to my students, colleagues, and mentors, who inspire me every day and without whom this work wouldn't be possible. www.gf.org/stories/anno...

Excited about Proofwala, @amitayush.bsky.social's new framework for ML-aided theorem-proving.

* Paper: arxiv.org/abs/2502.04671
* Code: github.com/trishullab/p...

Proofwala allows the collection of proof-step data from multiple proof assistants (Coq and Lean) and multilingual training. (1/3)

Some notes from our amazing panel discussion- ayushkhaitanrutgers.github.io/jmm.html

Looking forward to the #jmm2025 panel on the "Use of AI tools for Mathematics research" that we are co-organizing with @swarat.bsky.social and Amitayush Thakur. The panelists are Alex Kontorovich, Rishi Mehta, Emily Wenger and Kaiyu Yang. See you there!

Delighted to share our new position paper: arxiv.org/abs/2412.16075!

The o1/o3 path to math reasoning is based on LLMs and large-scale test-time search. We argue for a different path that uses formal proof assistants for
✅ creating high-quality synthetic data
✅ rigorous test-time feedback. (1/2)