Auxiliary Lemmas as Windows to Mathematical Surprise: Mining Unexpected Patterns in AI-Generated Proofs

AI tools sometimes invent mini-results (lemmas) while trying to prove things—let's see if these unexpected steps reveal new math patterns or proof strategies.

Research Question: Do auxiliary lemmas generated by AI-based theorem provers, such as Prover Agent, tend to highlight non-obvious or "unexpected" patterns in mathematical proofs, and can these patterns inspire new human-discoverable theorems?

Hypothesis: Auxiliary lemmas produced by AI systems frequently encapsulate nontrivial, reusable proof patterns or surprising intermediate results that human mathematicians may overlook, offering fertile ground for new conjectures or theorems.

Experiment Plan: - Collect and categorize auxiliary lemmas generated by Prover Agent and similar frameworks during automated proof construction.

• Identify recurring or novel lemma types not explicitly required by the main goal but helpful for proof completion.
• Involve human mathematicians to analyze these lemmas for patterns, generalizations, or entirely new research directions.
• Compare the conceptual complexity and explanatory power of these AI-generated lemmas with traditional human-devised proof steps.

References:

• Baba, K., Liu, C., Kurita, S., & Sannai, A. (2025). Prover Agent: An Agent-based Framework for Formal Mathematical Proofs. arXiv.org.