Leanimum-agent

@sudheerdotai Leanimum-agent (cmu-l3/Leanimum-agent) is a fully functional coding agent, so it has access to all bash inputs and outputs, including Lean checker errors, and can iteratively debug its proofs!

I’m honoured to be part of this project. Thanks to Zeyu @regunivers , a excellent researcher who leads the project and Jinbang @_chenjb who contributes a lot. I am happy to know many collaborators. Paper: zeyu-zheng.github.io: cmu-l3/reuF2Fagent: cmu-l3/Leanimum-agent

Amazing work and collaborative effort led by Zeyu Zheng (@regunivers)! Paper: zeyu-zheng.github.io Benchmark: cmu-l3/reuF2F Leanimum Agent: cmu-l3/Leanimum-agent (7/7)

paper: zeyu-zheng.github.io benchmark: cmu-l3/reuF2F agent: cmu-l3/Leanimum-agent 2/5 Why REU problems? Famous open problems (Erdős problems, Formal Conjectures) are great targets, but once one is solved the proof spreads fast, and a search agent can easily look it up. We really want a held-out evaluation! REU conjectures are a better fit. they are genuine open research questions, typically followed up by fewer people, so they are more likely to stay open, and unspoiled, for longer. We collected 244 problems from Duluth, Williams SMALL, MIT SPUR, Yale SUMRY, Polymath Jr. and more. The set has 45 problems in each of combinatorics, number theory, algebra, geometry & topology, and analysis, plus 19 Others. To preserve the benchmark's long-term utility, we encourage the community not to publicly release formalized solutions to benchmark problems.