Advancing mathematics research with AI-driven formal proof search
Large language models (LLMs) increasingly excel at mathematics tasks, but their unreliability limits their utility in mathematics research. A mitigation is to use LLMs to generate formal proofs in languages such as Lean, in which the compiler verifies every proof step. We present the first demonstration of this method’...
George Tsoukalas, Anton Kovsharov, Sergey Shirobokov et al.
· Science · 3 citations