Acorn and the future of (AI?) theorem proving

Summary

Acorn and the future of (AI?) theorem proving 30 Aug, 2025 Here's how mathematical proofs generally work. You start with some statement. Say, something like: Let G be a finite group. For all x∈G, there is some positive number k≤|G| such that xk=1. A standard mathematical proof is then a list of statements with the last one following from the previous ones: If G is a finite group, then consider the set S={1,x,…,x|G|}. Note that this set S is contained in the set of elements of G, which has size |G| Since there are |G|+1 powers of x in S, then there are at least two distinct powers in S, namely xn and xm with m<n which must be equal in value, xn=xm Therefore, xn−m=1 Since 0≤m≤n≤|G| then n−m≤|G| so k=n−m≤|G| works and we have xk=1 Now, someone might say, wait, hold on, why does step 2 imply 3? And then you might break it down slightly and say Since |S|≤|G| but our definition of S contains |G|+1 powers of x, there are only |G| possible values that xm can take on (for m∈{0,…,|G|}) But this must mean that at least two of these powers must match! Hence 3. And so on, until everyone agrees that, actually, the proof is good and we can accept the conclusion. Proofs in LeanOk, here's how proofs work in Lean. (I'll be taking the next example directly from the standard library.) To prove that an element has finite order in a finite order group, we start with variable [Finite G] lemma isOfFinOrder_of_finite (x : G) : IsOfFinOrder x := by by_contra h; exact infinite_not_isOfFinOrder h <| Set.toFinite _ which reads something like "Assume G is a finite group. We would like to prove this by contradiction: if there is an element y not of finite order in G, then the set of powers of y is not finite, so this set can't be contained in G. This implies that any element x∈G must be of finite order." Ok, fair enough, but that's pretty much almost assuming the claim via infinite_not_isOfFinOrder. Let's unpack what that is: theorem infinite_not_isOfFinOrder {x : G} (h : ¬IsOfFinOrder x) : { y :...