Reusing mathematical knowledge

Shuangping Li and Peng Zhang introduce GenLimitLib, a Lean library organizing results from 30 papers on generating valid new strings from examples.

Their September 29 preprint reports 79 successful proof runs out of 100 with a research sub-library, versus 48 with minimal definitions. Both conditions received the same papers and fixed theorem statements.

The evaluation covers five theorem tasks in one specialized area, not mathematics generally. It suggests that reusable formal knowledge can help AI proof development. The work remains a preprint; MathsAI has not reproduced the experiments.

References

• Original preprint
• Methods and results
• Paper PDF
• Library and paper map