Formalization of Bannai-Bannai-Stanton (Petrov-Pohoata)

Stream: mathlib4

[Antoine du Fresne von Hohenesche]

Hi everyone,

I have formalized the Bannai-Bannai-Stanton theorem (bound on distance sets in $\mathbb{R}^d$) following the proof by Petrov and Pohoata.

My goal is to contribute this to Mathlib. However, as I am a new contributor, I would appreciate guidance on the workflow. The code is fully working and the main theorem is proved, but it is currently written as a single monolithic file.

I am looking for advice on how to split the auxiliary results to fit Mathlib's hierarchy. Specifically, I have developed several lemmas that seem general enough to be upstreamed separately, including:

1. Combinatorics: An explicit bijection between restrictTotalDegree polynomials and Sym (Option (Fin d)) s to count monomials (using Sym.card_sym_eq_choose).
2. Linear Algebra: Bounds on the rank and inertia of matrices defined by polynomials (Polynomial Method / Croot-Lev-Pach lemmas).

I am unsure if there are existing Mathlib abstractions I should use instead of my manual counting arguments, or where these new lemmas should ideally live.

Here is the Gist with the full code:

https://gist.github.com/AntoineduFresne/184bb2f40f38d3592b80828f3a2ff525

Thanks for your help.

[Kevin Buzzard]

Out of interest, did you use AI in your proof?

[Antoine du Fresne von Hohenesche]

I utilized Gemini Pro 3 as an assistant for this formalization. It helped me with tactic discovery and syntax. My workflow often involved writing the proof strategy in natural language and asking the AI to help translate it into Lean or suggest tactics. I want to highlight two specific contributions from the AI: It mostly helped to construct the bijection for the monomial counting argument (using Option). For the rank bound (Croot-Lev-Pach Lemma Part 1), I intended to follow Petrov's proof, but the AI suggested a different, shorter trick to bound the rank (see comments in the code). I am unsure if this is the standard CLP proof or a (small) novelty, but the mathematical insight for that specific step came from the model.

[Kevin Buzzard]

I'm not in the area so I can't really comment on whether the result is in scope for mathlib, but I asked because your proof is extremely long and unidiomatic, which is the hallmark of an LLM-produced proof. I'm sure you don't want to hear this but one way of fixing this would be to actually learn how to write Lean yourself from one of the guides or online textbooks and then rewrite the proof in an idiomatic style. Right now LLMs are not capable of writing code which is anywhere near acceptable for mathlib.

[Antoine du Fresne von Hohenesche]

ok thanks for the information.

[Kevin Buzzard]

To pick on one of many examples, I think that only an LLM could come up with

        apply Exists.intro
        · apply Exists.intro
          · apply Exists.intro
            · apply And.intro
              on_goal 2 => apply Exists.intro
              on_goal 2 => { rfl
              }
              · simp_all only [not_false_eq_true]
              · simp_all only
          · subst hs
            simp_all only

There is basically nothing going on here and the LLM is writing meandering code.

[Kevin Buzzard]

You are one of many people recently who have come here asking "I have written an extremely long and unidiomatic proof using an LLM and would like to know how to get it into mathlib" and I am not entirely sure how the community should go about explaining to such people that unfortunately there is still typically a huge amount of work to be done before their sloppy code is anywhere near acceptable for the library.

The code quality review bar for mathlib is extremely high, for various reasons, and LLM-written code is very far from this bar right now.

[Antoine du Fresne von Hohenesche]

I completely understand. To be clear: I am not asking anyone to clean up this specific code for me. Since the file compiled, I was happy with the result, but I realize now that the code is sloppy and far too long for the library. You are right that the community needs to be clear with newcomers about this distinction, just as you were with me. I appreciate you taking the time to answer me directly.

[Peter Hansen]

@Antoine du Fresne von Hohenesche

You took the criticism like a champ. And while the proof is a bit messy, it’s sorry-free (which is already a real achievement). Now the fun begins: chipping away at the code line by line, sculpting it into a proof that can pass the scrutiny of the community.

I am not much more than a novice myself, but have few suggestions, you might want to consider:

Check your imports.

You only need:

import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.LinearAlgebra.Matrix.Rank
import Mathlib.LinearAlgebra.Matrix.BilinearForm
import Mathlib.RingTheory.MvPolynomial.Basic
import Mathlib.Data.Sym.Card

Explicit Variables in Definitions

In

noncomputable def distPoly {d : ℕ} {R : Type*} [CommRing R] :
  MvPolynomial (Fin (2 * d)) R :=
  ∑ i : Fin d,
    (X (Fin.castLE (by linarith) i) - X ⟨d + i, by omega⟩)^2

you might want to consider making d and R explicit, since they can not be inferred from other ones.

If you define,

noncomputable def distPoly (d : ℕ) (R : Type*) [CommRing R] :
  MvPolynomial (Fin (2 * d)) R :=
  ∑ i : Fin d,
    (X (Fin.castLE (by linarith) i) - X ⟨d + i, by omega⟩)^2

you can then write

lemma degree_distPoly {d : ℕ} {R : Type*} [CommRing R] :
    (distPoly d R).totalDegree ≤ 2 := by sorry

instead of

lemma degree_distPoly {d : ℕ} {R : Type*} [CommRing R] :
    MvPolynomial.totalDegree (distPoly : MvPolynomial (Fin (2 * d)) R) ≤ 2 := by

Merge Lines

There places, where you do rewrites on one line and then again on next one. If the line length permits it, consider merging them into a single line. The same goes for obtain. You can write:

obtain ⟨w, w_1,w_2, left, w_3, rfl⟩ := hr

which is shorter than

obtain ⟨w, h⟩ := hr
obtain ⟨w_1, h⟩ := h
obtain ⟨w_2, h⟩ := h
obtain ⟨left, right⟩ := h
obtain ⟨w_3, h⟩ := right
subst

Here is a version of your code with a few improvements. It cuts away just above 100 lines of code. It small step in the right direction, I think.

[Kevin Buzzard]

Yes, a sorry-free proof is a great achievement! We have an entire course at Imperial whose goal is to get people to sorry-free proofs and spend no time encouraging people to get stuff into mathlib -- it's all about the theorems. I didn't make these encouraging noises because I just answered the question because I'm a bit autistic. And turning a sloppy proof into a mathlib-ready one is probably a lot easier than writing a mathlib-ready one from scratch (unless it turns out that the entire approach is not mathlib-suitable, which I can't comment on because I'm not in the area). My general impression is that there are too many definitions but really you should be talking to experts in the area if you really want to tidy this up for possible inclusion into mathlib and are not content to just say "yay I did it". Note that I am not attempting to get FLT into mathlib, I am just attempting to say "yay I did it".

[Antoine du Fresne von Hohenesche]

Thank you Peter for the concrete help. I really appreciate you taking the time to review the code and especially for sharing the refactored version. I hadn't realized how bloated my imports were, and your point about merging the obtain lines is exactly the kind of idiomatic syntax I was missing (as Kevin noted, that block was definitely an artifact of me fighting the goal state step-by-step). I will update the gist.

Thank you Kevin for the follow-up and the context regarding the "sorry-free" achievement. I genuinely value the honesty—it saves me from having unrealistic expectations.

To provide a bit of background, this formalization is actually a 2-3 week project for a course I am taking at ETH Zürich. So, in the immediate term, reaching the "sorry-free" state to verify the theorem was the primary academic goal, and I am quite happy to just say (as you put it) "yay I did it" for the purpose of the grading.

That said, I am still very interested in learning how to do this properly. I have another Lean project to do (again something combinatorial: Davenport-Schinzel Sequences).

I do think my current file contains several results which could belong in Mathlib independently (e.g., bounding the rank of the sum of two matrices, the Croot-Lev-Pach lemma, or the linear independence of functions via the diagonal argument... maybe they are already there, but I didn't find them). For now, the code could be much shorter if some of these foundations were already in place. So maybe it is more reasonable to wait or participate in the formalization of these "simpler" lemmas first, rather than trying to upstream a theorem that requires all of them at once. It feels like I tried to forge a sword by brute force from scratch in the wild, instead of waiting for a proper furnace to make it.

Thanks again to you both.

[Yaël Dillies]

Out of historical interest, Croot-Lev-Pach was already done in 2019: https://lean-forward.github.io/e-g/e-g.pdf

[Matthew Coke]

I'd suggest that an intermediary mechanism be created to link llm created "proofs" to editors for translation to mathlib. I'm a fan of the earth-fire-water abstract triplet where, in this case, llms are earth, fire is the editors that do the translation, and our source of truth, as close as we can get to it anyway, is mathlib. llms might produce slop but, in somewhat defense of them..they can produce a lot of slop? That triplet mechanism is rather generalizable, maybe it can find a place in Lean as well?