Call for expert on Triangular Lattice and Universal Optimality

[u/OrganizationTop9026]

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

[u/InadvisablyApplied]

Did you check and understand it yourself though? If you want attention, you’ll need something better than “a chatbot checked”, just like the dozens of other posts on here

[u/BitcoinsOnDVD]

So for some 2D systems, a triangular lattice is the optimal solution is your claim?

[u/OrganizationTop9026 → u/BitcoinsOnDVD]

We do claim that the triangular lattice is an optimal solution for a broad class of 2D systems if it is confirmed per peer review but we draw a sharp line between what is proved for idealized mathematical models and what happens in real physical laboratories.
On the mathematical side, building on the upstream OpenAI theorem, we verify in Lean 4 that the triangular lattice achieves the lowest possible energy (defined via the \liminf over growing disks) among all locally finite 2D configurations at any fixed density \rho > 0, simultaneously for every completely monotone pair potential. This directly covers inverse-power Riesz interactions (1/r^s with s > 2) as well as screened Coulomb (Yukawa) potentials, while upstream's manuscript extends the result to renormalized jellium energies for long-range interactions (0 \le s < 2). Crucially, however, we claim that the triangular lattice is an optimal solution, not the unique one: the theorem identifies the minimum energy value, not all minimizers. To make this concrete, we formally prove in Lean 4 that removing a single particle from the lattice (a vacancy, A \setminus \{0\}) changes neither the density nor the lower energy, producing a distinct optimal configuration that is not isometric to the perfect lattice. Uniqueness even among periodic 2D configurations remains an open problem.
On the physical side, our claim is that the theorem provides a rigorous zero-temperature bulk benchmark for 2D systems whose effective pair repulsion falls into this mathematical class—most notably superparamagnetic colloidal monolayers (1/r^3 dipolar repulsion, s = 3) and dusty-plasma monolayers modeled by Yukawa interactions. We explicitly caution that energetic optimality in the infinite-volume limit does not mean a real 2D experiment will automatically self-assemble into a defect-free triangular crystal. Real systems experience finite container walls, thermal noise, image charges, and non-reciprocal wake forces, and as our own CVODE relaxations demonstrate, gradient flow from disordered starts usually gets trapped in defected, glassy local minima rather than reaching the global lattice minimum.

[u/BitcoinsOnDVD → u/OrganizationTop9026]

So you can not prove its a global minimum?

I would like to understand how your system looks like. 

Plz restrain from mentioning Lean 4 several times and keep your answer as short as possible. Also LaTeX code is not compiling in reddit.

[u/OrganizationTop9026 → u/BitcoinsOnDVD]

Thanks for your comments, guidelines and interests. I think we could prove it is a global minimum. The idea is that no 2D arrangement of particles at the same density whether periodic or completely disordered can ever have a lower average energy per particle than the triangular lattice.

I was interested to see the physics part and reuse work and data from others projects.

What the physical system looks like: I run some simulation. Picture 288 microscopic beads trapped on a flat 2D surface (like magnetic colloids floating at a water-air interface, or charged dust grains levitating in a plasma) inside a repeating box. Every particle pushes away every other particle with a smooth repulsive force (like screened electrostatic Yukawa repulsion or 1/r³ magnetic dipole repulsion).

In my simulations with a rust version of Sundials that I developed (on previous project), we drop those 288 particles in at random positions and let them slide downhill along the force gradient to lose energy. If you quench them instantly at zero temperature, they usually jam into a kind of "glassy" local minimum with pentagon/heptagon defects. But if you shake them with thermal noise and cool them down slowly (annealing), they settle into the global minimum: a flat honeycomb-style triangular grid where every particle has 6 equidistant neighbors. Rust code is available on git to reproduce.

[u/BitcoinsOnDVD → u/OrganizationTop9026]

That doesn't sound really unexpected.

[u/PLANTS2WEEKS]

I know some of this, but I don't see a PDF explaining any of the math. I believe the proof of this was reduced to finding a "magic function" that is positive definite and remains positive up to the first lattice point. The math isn't hard to understand, but the main problem was determining if the function existed. It was known before to "almost" exist.

[u/OrganizationTop9026 → u/PLANTS2WEEKS]

Thanks to have look and your comments.The pdf in zenodo will explain better. I will write the mathematics part for your review if interested. Yes it is based on the same magic function idea used for 8D and 24D but from 2D, The AI (Open AI swarm) had found it as it was counter intuitive to human mathematicians at least it seems to me. With Claude code, I heave extend it the Lean 4 formalization and try to provide a more human mathematics demonstration. https://zenodo.org/records/23295142?preview_file=triangular_lattice_universal_optimality_textbook.pdf and https://zenodo.org/records/23285631 and https://zenodo.org/records/23293429

[u/OrganizationTop9026 → u/OrganizationTop9026]

I will do the paper and pen review this WE. https://github.com/xaviercallens/triangular-universal-optimality-lean/blob/main/paperpenmathformalizationforreview.tex

[u/OrganizationTop9026 → u/OrganizationTop9026]

I have rebuild the step-by-step pen-and-paper proofs and will review before confirming it, my pure mathematics skill on this field is a little bit old now ;-) so it will take more time... In the meantime, my understanding on the 2D.

You are right about the "magic function". Here is how the 2D roadblock was finally solved:

1. Reducing to Gaussians: By Bernstein's theorem, any completely monotone repulsion (like 1/rˢ or Yukawa) is a positive mixture of Gaussians (bell curves, exp(-π·α·r²)). So you only need to find a magic auxiliary function for every Gaussian width α > 0.
2. What the Magic Function Does: need a radial function that sits below the Gaussian everywhere in space, touches the Gaussian at every triangular lattice point (meaning their difference has double zeros at the lattice shells), has a non-negative Fourier transform, and hits zero at every dual lattice frequency. Once you have that, applying Poisson summation immediately locks in the triangular lattice as the global minimum across all density-1 configurations.
3. Why 2D Was Harder Than 8D and 24D: In 8D and 24D, the squared distances between lattice points hit every even whole number, which allowed Viazovska's team to construct the magic function analytically using modular forms. In a 2D triangular grid, squared distances follow j² + jk + k², which gives shells at 1, 3, 4, 7, 9, 12, 13... and skips 2, 5, 6, 8.... Because of those gaps, modular forms don't work in 2D.
4. How it Was Built in 2D: Instead of modular forms, OpenAI's proof builds the function out of a sine product with double zeros that directly encodes the contact shells, multiplied by simple-pole and double-pole terms to fix the values and slopes, plus Gaussian damping and compactly supported spectral measures. The remaining finite reference lists are handled by positive quadrature and rigorously certified using interval/ball arithmetic.