Improving the tools around the prover

Jules Viennot and colleagues let AI propose interface changes, retaining those that helped smaller models prove mathematics. Their September 30 preprint, revised October 1, reports improved Rocq benchmark performance.

Transfer to Lean was mixed: the interface solved fewer problems than an established alternative, while reducing cost and time on problems solved by all compared systems.

The findings concern benchmark proof tasks, not new mathematical discoveries. The study remains a preprint; MathsAI has not reproduced it.

References

• Original preprint
• Methods and results
• Paper PDF
• Code and experiments