Subscribe to Events
O-Forge: a verifiable, LLM-driven framework for proving inequalities in research mathematics.
Ayush Khaitan
Location: CoRE 431
Date & time: Wednesday, 05 November 2025 at 1:30PM - 3:00PM
We introduce an LLM + computer software framework for proving sophisticated inequalities in research mathematics. We first ask a frontier LLM to break up a problem into its simplest parts, and then ask a computer algebra system to complete the proof for each part. In doing so, we resolve a problem posed by Terence Tao about AI for Mathematics. This is joint work with Vijay Ganesh (Georgia Tech).