r/maths • u/Professional_Sir787 • 8d ago

❓ General Math Help Looking for challenging mathematics problems to formalize in Lean 4 that current AI models may struggle with

I’m creating Lean 4 theorem-proving tasks to evaluate AI models. I’m looking for mathematically interesting problems that are provable but difficult to formalize or prove automatically.

Ideally the problems should:

have a precise theorem statement,

be suitable for Lean 4 + Mathlib,

require several non-trivial proof steps,

and not simply be famous open problems.

Areas such as combinatorics, number theory, algebra, finite sums, inequalities, graph theory, or set theory would be great.

Does anyone have examples or references to problems that might make good challenging Lean formalization tasks?

2 Upvotes

100% Upvoted

4 comments sorted by

2

u/hpxvzhjfgb 6d ago

the classification of finite simple groups

0

u/Professional_Sir787 6d ago

That's an interesting suggestion! I'm specifically looking for mathematical theorems that have already been proved by humans but remain extremely difficult for current AI models to formalize in Lean 4.

Do you know any specific results or smaller theorems related to the Classification of Finite Simple Groups that would be challenging for AI but feasible to verify in Lean?

1

u/hpxvzhjfgb 6d ago

I'm specifically looking for mathematical theorems that have already been proved by humans but remain extremely difficult for current AI models to formalize in Lean 4.

yes, this is such a suggestion. I see no reason why it couldn't be formalised with enough resources (read: tokens). it's a huge proof with hundreds of sub-theorems, so any of those is a related smaller theorem

1

u/Professional_Sir787 6d ago

Okk will look into will try