Formalizing Gardam's disproof of a "Kaplansky Conjecture"

Stream: lean4

[Siddhartha Gadgil]

A few months ago, Giles Gardam disproved a long-standing conjecture - often called Kaplansky's Unit conjecture, a very basic statement in Algebra.

@Anand Rao and I have formalized this proof in lean 4 at https://github.com/siddhartha-gadgil/Polylean/tree/main/Polylean. The README in that folder gives an outline of the code. Our proof mixes proving with some computation, and part of our motivation was to use the nature of lean 4 as a theorem prover as well as a programming language with both aspects integrated.

More details will follow soon in a blog post or two. Comments and suggestions are very welcome.

[Kevin Buzzard]

Oh nice! I suggested to an MSc student that they tried formalising Gardam's work in Lean 3 but we ended up doing something else. The different models for the fg group in question looked to be to be the scary part.

[Siddhartha Gadgil]

Thanks.
One just has to use one of the models, and we used the description as a Metabelian group. Gardam explicitly gives the data needed: the group action and the cocycle.

We took advantage of the programming capabilities of lean 4: using the Decidable typeclass the 64 checks for being a cocycle became just by decide with automation by typeclass inference.

[Kevin Buzzard]

It had not occurred to me to try lean 4 for this -- my instinct would have been "well you'll have to make free abelian groups etc, just stick with lean 3".

[Siddhartha Gadgil]

Mathlib4 has abelian groups, though not homomorphisms. We did have to define being free etc, but this meant we could do this effectively, so equality of homomorphisms is decidable for finitely generated free abelian groups. We clearly redid some stuff which is ready with mathlib, but that was not that much work (a few days work for @Anand Rao and myself).

[Sebastian Ullrich]

Nice work, that must surely be the first mathematical proof of this size in Lean 4. I'm a bit surprised at the lack of a lakefile.lean, how did you even develop the project?

[Siddhartha Gadgil]

Thanks.
There is a lakefile.lean. My link was to a sub-folder of an existing project. The project is at https://github.com/siddhartha-gadgil/Polylean.

[Anand Rao]

Thank you. The link is actually to a sub-folder of the main folder containing the relevant code. The project contains a lakefile.lean in the outermost directory (https://github.com/siddhartha-gadgil/Polylean/blob/main/lakefile.lean).

[Sebastian Ullrich]

Oh my, I completely missed that!

[Anand Rao]

Siddhartha Gadgil said:

Mathlib4 has abelian groups, though not homomorphisms. We did have to define being free etc, but this meant we could do this effectively, so equality of homomorphisms is decidable for finitely generated free abelian groups. We clearly redid some stuff which is ready with mathlib, but that was not that much work (a few days work for Anand Rao and myself).

Adding to this, the key requirement for defining the group P was actually the Metabelian group construction, which turned out to be fairly short and self-contained (requiring only homomorphisms and group actions). We could have in principle done without the theory of free Abelian groups, but as @Siddhartha Gadgil mentioned, we did this to automate the checking of the cocycle condition.

[Patrick Massot]

Siddhartha Gadgil said:

We took advantage of the programming capabilities of lean 4: using the Decidable typeclass the 64 checks for being a cocycle became just by decide with automation by typeclass inference.

Does this use of the computation power of Lean 4 means you also trust more or is it still using Lean 4 without extra axioms?

[Siddhartha Gadgil]

In the last stage we had to use native_decide. In principle by decide should work but in practice it times out. The algorithms are far from optimal, but I don't know if that is the key bottleneck, or whether once per module compilation lands things will just work.

[Siddhartha Gadgil]

We did not introduce axioms though. It is functions returning Decidable P strung together by typeclass inference.

[Siddhartha Gadgil]

And the part I mentioned automating: showing that we have a cocycle and a group action, is entirely using by decide, so no trust issues.

[Sebastian Ullrich]

Just to be clear, per module compilation (as in compilation to native code) will make native_decide faster, but not decide

[Siddhartha Gadgil]

I see. native_decide is instantaneous already. Is there some way to bridge the gap?

[Siddhartha Gadgil]

Or should one accept native_decide as safe?

[Siddhartha Gadgil]

I had a variant of the approach where instead of by decide or by native_decide I used apply to reduce to a certain Boolean function being true. However rfl or simp on that function timed out too.

[Sebastian Ullrich]

There are some plans for improving symbolic reduction that should help with decide, but no concrete time frame yet afaik

[Sebastian Ullrich]

It makes sense that rfl in that context would do roughly as much work as decide, yes

[Siddhartha Gadgil]

For the present then I will use native_decide wherever needed.

[Siddhartha Gadgil]

In case anyone is interested, I have written a blog post with some details: https://siddhartha-gadgil.github.io/automating-mathematics/posts/formalizing-gardam-disproof-kaplansky-conjecture/

[Laurent Bartholdi]

Very nice!
I should mention that this has been also formalized in Lean3, by @Cedric Holle . We did run into lots of difficulties because of lean3's performance, and had to run through complicated hoops to get the proof accepted in reasonable time. I was sure @Cedric Holle had posted his code, but can't find it; hopefully he can comment.

[Kevin Buzzard]

In some weak sense I am more impressed by the Lean 3 proof because clearly Lean 4 is a much better tool for doing this job ;-)

[Cedric Holle]

Laurent Bartholdi said:

Very nice!
I should mention that this has been also formalized in Lean3, by Cedric Holle . We did run into lots of difficulties because of lean3's performance, and had to run through complicated hoops to get the proof accepted in reasonable time. I was sure Cedric Holle had posted his code, but can't find it; hopefully he can comment.

You can find my code here: https://github.com/todbeibrot/counter-example-to-the-unit-conjecture-for-group-rings
It needs ~6GB of memory and it takes some time. Also, I didn't add any comments and some things are quite inelegant.