Choosing useful mathematical context

Sareh Nabi and colleagues test MathAgent, which supplies AI theorem provers with relationships between mathematical statements. Their September 28 preprint compares four context settings across five models using Lean 4.

The authors report that specialized training mattered more than added context. Knowledge graphs helped smaller models but hindered larger ones. Different settings nevertheless solved different problems, suggesting room for adaptive selection.

The reported best-case combination assumes an ideal selector; it is not a demonstrated routing system. This preprint does not establish new mathematical discoveries, and MathsAI has not reproduced its experiments.

References

• Original preprint
• Paper PDF
• Project repository