Choosing what to prove

Niket Patel and colleagues propose training AI to favor concise statements requiring comparatively long proofs. Their September 23 preprint uses this measurable proxy to guide conjecture generation in Lean.

Among verified samples, the authors report substantially less overlap with Mathlib after training. An AI judge assessed that overlap; absence from one library does not establish worldwide novelty.

Proof length depends on coding style, and the future usefulness of generated results remains uncertain. This is an early discovery experiment, not a settled measure of mathematical importance. MathsAI has not reproduced it.

References

• Original preprint
• Methods and limitations
• Paper PDF