For those interested in Triangular Lattice and Universal Optimality, I'd appreciate some second eyes on something I've been working on.

My objective was to leverage some OpenAI and Anthropic formal mathematics undirected claims to make it more valuable to the scientific community with my experience in AI assisted proof and Lean 4 formailzation where I could contribute more. On this undirected math formal proof (their brutal force algorithm was not guided to some specific interested apparently), I find some interesting progress what could lead to the universal optimality in 2D. To go further, it needs a mathematics and physics expertises in the field, which was already proven for 8D and 24D. cf. paper published in the Annals of Mathematics in 2022 titled "Universal optimality of the $E_8$ and Leech lattices and interpolation formulas," mathematicians Henry Cohn, Abhinav Kumar, Stephen D. Miller, Danylo Radchenko, and Maryna Viazovska

The topic seems to me to be an interesting result leveraging the last OpenAI math lean 4 contribution : in a plane, if particles repel each other in a certain broad class of ways, the triangular (honeycomb-like) arrangement has the lowest possible energy. The proof was recently checked by formal proof (in Lean 4, the proof assistant). The document tries to explain it in three ways side by side: the ordinary proof step by step, the computer-checked version, and small numerical experiments in Python and Rust with Solver. One chapter connects it to fluid dynamics (point vortices, vortex crystals) and a few other physical systems that some physicians may be perhaps interested in.

Over the past weeks I put articles together and a textbook with the help of AI tools (Claude). I directed the work and I'm responsible for it, but I want to be upfront that most of the writing was AI-assisted and that no expert has reviewed it yet. That's the reason for this post....

I've tried to be careful about what is actually proven and what is only an argument or a numerical hint. Each claim is labelled with how far to trust it. But I'm sure there will be mistakes or limitations that I can't see. There's already one I know of: a numerical shortcut in an earlier paper mattered more than I first said, and it's noted in the text book.

If you have time, interest and expertise, it would help a lot to peer review https://github.com/xaviercallens/triangular-universal-optimality-lean

cf PDF https://github.com/xaviercallens/triangular-universal-optimality-lean/blob/main/docs/physicist_guide/guide.pdf and https://zenodo.org/records/23295142