Reposted by Ayush Khaitan
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...
April 16, 2025 at 7:41 AM
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...
Reposted by Ayush Khaitan
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)
* 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)
February 22, 2025 at 9:32 PM
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)
* 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
January 17, 2025 at 10:53 PM
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!
January 3, 2025 at 10:02 PM
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!
Reposted by Ayush Khaitan
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)
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)
December 23, 2024 at 2:49 PM
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)
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)