Lean proofs obtained and formalized with use of AI models, namely some combination of Claude Opus 5/5.5, Claude Fable 5/5.1, GPT-5.6 Sol and GPT-6 Astra. I've tried to assert the novelty of these proofs: all are pending comprehensive human validation and formal writeups. Each Lean file imports only Mathlib.
MISC PROOFS (RESULTS THAT SEEM SIGNIFICANT BUT DO NOT CLOSE AN EXPLICIT OPEN PROBLEM/CONJECTURE)
PROOFS THAT CLOSE AN EXISTING OPEN PROBLEM/CONJECTURE OR IMPROVE A BEST PUBLISHED BOUND:
Problem 18 - First machine-checked solution of LLQTW Problem 1.8: a zero-error average-case polynomial-time algorithm for orthogonal and unitary 3-tensor isomorphism over all finite fields, fully formalized and kernel-verified in Lean 4.
BalancedOrdinaryReduction.lean - Addresses Grochow and Qiao’s Open Question 10.8 on near-optimal reduction from d-tensor isomorphism to three-tensor isomorphism. Over every field, exact isomorphism equivalence and total output dimension O(n^⌈d/3⌉) are formally verified for arbitrary ordered shapes with d ≥ 3 and factor dimensions bounded by n ≥ 2, with an absolute implied constant. This achieves the requested exponent asymptotically as d grows and the counting-bound exponent when 3 divides d; the polynomial-time construction remains a written argument rather than a formally verified running-time theorem. Improves the published dimension exponent from (\lfloor d/2\rfloor) to (\lceil d/3\rceil), a strict improvement for six factors and every order at least eight: six-way tensors require output dimensions (O(n^2)) instead of (O(n^3)), and twelve-way tensors require (O(n^4)) instead of (O(n^6)). Published baseline: https://opus.lib.uts.edu.au/bitstream/10453/189643/2/3717823.3718282.pdf
When three divides (d), the reduction attains the finite-field counting lower-bound exponent: uniformly sized inputs can be encoded as ordinary three-tensors with only (O(n^d)) output coordinates—linear in the input’s coordinate count—while preserving and reflecting isomorphism exactly. This provides an optimal exponent for infinitely many orders and approaches the optimal exponent as (d) grows, addressing Grochow–Qiao’s quantitative order-reduction question.
Lean verifies correctness and the absolute-constant dimension bound over every field, for arbitrary ordered shapes with (d\ge3) and factor dimensions bounded by (n\ge2); polynomial running time remains a written argument.
PlateauedAdditionDesigns_BorderedRankCharacterization.lean — A self-contained, Mathlib-only answer to Open Problem 4 of Hyun–Kwon–Wang–Wu, Designs, linear codes, plateaued functions, and their interconnections (2026). For every (r\ge1) in the nondegenerate parameter range, replaces Theorem 3(iii)’s rank-plus-Reed–Muller embedding condition with the single criterion (\operatorname{rank}_2!\begin{pmatrix}M&\mathbf1\\mathbf1^T&0\end{pmatrix}=m+2). Proves equivalence with an (r)-plateaued addition-design realization having no nonzero linear structures, including the full reconstruction. Also constructs a simple (2\text{-}(64,28,24)) design of incidence rank (9) showing that the original, unbordered rank condition alone is insufficient already for (r=1).
CubicBentSupportCodeDesignAutomorphismGroups.lean — A Mathlib-only formalization answering Open Problem 6 of Hyun–Kwon–Wang–Wu, Designs, linear codes, plateaued functions, and their interconnections (2026) for an infinite family of cubic bent functions with arbitrary quadratic stabilization. The problem asks for simpler, explicit automorphism groups for special bent functions. This proof determines both the full support-code and support-design automorphism groups, replacing Theorem 8’s abstract stabilizer description with an explicit semidirect-product structure, multiplication laws, and exact group orders. It resolves the requested determination for this family—not a classification of all bent functions.
TwoAnchorWalshMUBClassificationAndExtensions.lean - A Mathlib-only proof incorporating the resolution of Open Problem 3.65 in Polujan’s Boolean and Vectorial Functions (2021) and extending it to real Walsh MUB configurations. For vectorial bent maps in the admissible Nyberg range, vanishing-flat design isomorphism, extended-affine equivalence, and arbitrary complex unitary equivalence preserving the computational and Walsh bases individually are equivalent. Constructs the normalized family of (2^m+1) real MUBs in dimension (2^N), and proves that an additional Walsh-phase basis is unbiased to the family exactly when adjoining its Boolean phase preserves vectorial bentness; the resulting enlarged family explicitly contains the original bases. Subsumes the earlier vanishing-flat classification and Walsh-phase extension proofs. The two-anchor restriction is essential: no unanchored classification or restriction on arbitrary additional complex bases is claimed.
CompleteSevenMUBDegreeFiveParent.lean - A Mathlib-only proof extending the polynomial-parent approach in Designolle’s Most incompatible measurements and sum-of-squares optimisation (2026). Every hypothetical family of seven MUBs in complex dimension six admits an explicit degree-five parent POVM with depolarizing visibility (56137/184289) and generalized visibility (232487/552867), strictly improving the retained (4415/14497) construction. Also proves the exact attained optimum within the common-quadratic odd-sum-of-squares parent class, including finite sums: the largest real root of (42875\eta^3-12495\eta^2-609\eta+133=0). The proof establishes the required conditional moments, positivity, normalization, and every marginal from the actual MUB hypotheses. This is a restricted-class optimum—not the optimum over all joint measurements—and does not establish that seven MUBs exist.
FourProjectiveMeasurements_ArbitraryRank_LowerBoundAndRigidity.lean - A proof of the arbitrary-rank four-measurement selected-sum bound, resolving the four-measurement case left open after Theorem 9 of Designolle–Farkas, k-fold unbiased measurements and maximal incompatibility (2026). Covers every outcome count (n\ge2) in every positive finite dimension, allowing unequal and zero outcome ranks without assuming unbiasedness. Also proves equality rigidity: attaining the bound forces every subtriple to be algebraically three-fold unbiased.
PairwiseUnbiasedPVMTripleCompatibility.lean — A Mathlib-only proof extending Designolle–Farkas, k-fold unbiased measurements and maximal incompatibility (2026). Every arbitrary-rank triple of pairwise mutually unbiased projective measurements with (n>0) outcomes admits an explicit positive normalized parent at generalized visibility ((1+x_n)/3), where (x_n) is the unique positive root of (n^2x^3-3nx-2=0). This resolves the pairwise-unbiased special case of Conjecture 10(3,4). For every rank-one MUB triple in dimension (n\ge3), the same parent achieves a strictly larger visibility with an explicit, dimension-dependent positive increment, replacing the earlier compactness-only existence result. The proof includes a quantitative flat-unitary inequality and exact sum-of-squares control of all marginal cross terms. All earlier results, including (x_4=\cos(\pi/9)), are retained. The unrestricted arbitrary-PVM conjecture and dimension-six MUB existence problem remain open.
PolujanPottV1.lean - An affirmative answer to Polujan-Pott (2021) Open Problem V.1 / Polujan's (2021) Open Problem 3.64: "Can two vectorial bent functions have isomorphic graph translation designs without being EA-equivalent?"
Polujan365.lean - An affirmative answer to Polujan’s (2021) Open Problem 3.65: “For every even (n), are two vectorial bent functions EA-equivalent exactly when their vanishing-flat designs are isomorphic?” Here it is proved that vanishing-flat design isomorphism is equivalent to EA-equivalence for all vectorial bent functions in the admissible Nyberg range.
Polujan369.lean - A negative answer to the realizability question in Polujan’s (2021) Open Problem 3.69: “Must a subdesign of a vectorial bent function’s vanishing-flat design, with the parameters expected of an extension, itself arise from such an extension?” Here a six-variable vectorial bent function F: F₂⁶ → F₂² and a 2-(64,4,3) subdesign of VF(F) are formally verified in Lean, together with the impossibility of realizing that subdesign as VF((F,g)) for any Boolean coordinate g. This resolves the realizability question within the admissible Nyberg range; the separate subdesign-existence question is not addressed.
BentAffineOrbit.lean - An affirmative answer to Kudin, Pasalic, Polujan, and Zhang’s (2025) Open Problem 2: “Can one construct EA-inequivalent bent concatenations outside the completed Maiorana–McFarland class using affine rearrangements of one fixed seed?”; here an explicit pair is formally verified in every even dimension N ≥ 8, with distinct linearity indices N/2 − 2 and N/2 − 1, together with an exact rank formula for concatenations from rigid seeds.
PermanentDeterminantalLowerBound_CharZero_AllSizes.lean - A proof that every size-(m) affine determinantal representation of the (n\times n) permanent over any characteristic-zero field satisfies (n^2\le 2m), strengthened to (n^2+1\le 2m) whenever (n\ge3). The result completely subsumes Mignon–Ressayre’s Theorem 2 from A quadratic bound for the determinant and permanent problem (2004), recovered as an explicit corollary. It improves the integer lower bound by one for every even (n\ge4), while matching the original rounded bound for odd sizes.
BentDesignRank.lean - A refutation of Hyun, Kwon, Wang, and Wu’s (2026) Open Problem 7: “Do the designs D_{g,h} and TD_h in Theorem 10 always have equal binary ranks?”; here an explicit eight-variable counterexample is formally verified in Lean, satisfying every bent-function and duality hypothesis, with binary ranks 29 and 30 respectively.
MetricRegularBent.lean - An affirmative answer to Meidl, Polujan, and Pott’s (2023) Question 5.16: “Can the set C_F for some (n,m)-bent function F be metrically regular?” Here the code C_q = RM(4,1) + ⟨q⟩ for q = x₁x₂ + x₃x₄ is formally proved equal to its double metric complement. The formalization also verifies that q is extendable by exhibiting g such that q, g, and q + g are all bent. This establishes the requested existence for an extendable (4,1)-bent function; literature priority remains unverified.
DMT17.lean - An affirmative answer to Ding, Munemasa, and Tonchev’s (2019) Conjecture 17: “For each fixed admissible output dimension, does the number of inequivalent codes obtained from vectorial bent functions grow exponentially, with the proportion admitting a two-transitive automorphism group tending to zero?” Here both assertions are formally proved, with the stronger conclusion that even the proportion admitting a transitive automorphism group tends to zero, and quantitative bounds uniform across all admissible output dimensions.
ProductBasisErrorOptimumAndFourMeasurementSpectralBounds.lean — A Mathlib-only proof that four orthonormal product bases in (\mathbb C^2\otimes\mathbb C^3), including indirect bases, have minimum total squared unbiasedness error exactly (2/3), with explicit attainment and complete classification of all minimizers. Resolves a special case of the arbitrary-rank spectral-bound extension explicitly left open after Designolle–Farkas’s Theorem 9: four projective measurements containing a pairwise mutually unbiased triple, with any fourth PVM. Also proves sharp product-basis minimax corollaries and a strict dimension-six spectral improvement of (1/583200). The unrestricted conjecture remains open. Fully Lean-verified using only Mathlib, without placeholders or custom axioms.
FiveIsoentangledETF.lean — A proof that every two-qubit entanglement spectrum admits a five-state equiangular tight frame. Gives an explicit construction spanning product to maximally entangled states, with squared pairwise overlap 1/16 and frame operator (5/4)I. Provides a uniform analytic solution to the existence question explored numerically in Section IV of Wei–Cobucci–Tavakoli, Nonprojective Bell-state measurements (2024).
ETFAllDimensionsAllPurities.lean — A proof that every integer d ≥ 2 admits an equiangular tight frame of d² + 1 normalized bipartite states with any prescribed common reduced purity p ∈ [1/d, 1]. Includes the maximally entangled endpoint, answering the higher-dimensional existence question in Section IX of Wei–Cobucci–Tavakoli’s Nonprojective Bell-state measurements (2024), and extends Section IV’s entanglement-tuning observations to all dimensions at the level of purity.
MaximallyEntangledTightFrame_ExactOneWayPPTOptimum.lean - Proves that every maximally entangled tight frame of (N) states in (\mathbb C^d\otimes\mathbb C^d), for (d\ge2), has exact uniform-prior, single-copy discrimination optimum (d/N): an explicit one-way protocol achieves it, and no PPT measurement can exceed it. Includes the exact five-state qubit value (2/5), resolving the numerical one-way shortfall reported by Wei–Cobucci–Tavakoli (2024), Section VII.
FiveStateRegularSimplex_TwoCopyGlobalOptimum.lean - Proves that two identical copies of any five-state regular simplex, sampled uniformly, have exact global discrimination optimum ((13+4\sqrt3)/20 \approx 0.9964101615). Constructs an attaining POVM and proves a matching universal upper bound, giving an exact regular-simplex formulation of the numerical result reported by Wei–Cobucci–Tavakoli (2024), Section VII.
JouxNarayanan54.lean - An affirmative answer to Joux–Narayanan’s Question 5.4: “Does ordinary tensor isomorphism reduce to tensor isomorphism under special-linear transformations?” Here zero-padding each mode from dimension n to 2n is formally proved to preserve and reflect equivalence over every field, for arbitrary input tensors. The proof certifies an explicit coordinate projection with exactly eight times as many output entries, establishing TI ≤ TI_SL.
TIEqTISp.lean - A partial answer to Chen, Grochow, Qiao, Tang, and Zhang (2024)'s Open Question 8: "Which, if any, of TI_O, TI_U, TI_Sp are equal to TI?"; here it is proved that TI = TI_Sp.
TIParStandalone.lean - Resolves the maximal-parabolic case of Chen, Grochow, Qiao, Tang, and Zhang’s (2024) research direction in §1.5: “What are the tensor-isomorphism complexity classes associated with other matrix groups, including parabolic subgroups?”; here TI = TI_Par is proved for the maximal parabolic family P_(n,n) over every field, under coordinate-projection reductions with polynomial output-size bounds. This addresses an explicitly proposed research direction, rather than a numbered open question.
FormTI.lean - A partial answer to Chen, Grochow, Qiao, Tang, and Zhang (2024)’s Open Question 1.11: “What is the complexity of tensor isomorphism restricted to other form-preserving groups, including mixed orthogonal groups and groups preserving forms that are neither symmetric nor skew-symmetric?”; here TI-completeness is proved for seven form-isometry families, including O(n,n), O(3n,n), and families preserving nonsymmetric or degenerate bilinear forms, under coordinate-projection reductions with polynomial output-size bounds.
TStarUnimodality.lean - A complete answer to Iršič, Klavžar, Rus, and Tuite’s (2024) Problem 5.2: “Which thick grids have unimodal general-position polynomials?” For m = min(r,a) and n = max(r,a), non-unimodality holds exactly when m = 2 and n = 8; m = 3 and 11 ≤ n ≤ 17; or m ≥ 4 and 2m + 4 ≤ n ≤ m + (m + 1)(1 + (m − 1)!). The classification is formally verified in Lean for all positive parameters, including the graph-counting formula and every exceptional case; literature priority remains unverified.
FangCounterexample.lean - A refutation of Fang’s (2017) Conjecture 2.9: “Does identical collapse tomography at every vertex imply that a graph is vertex-transitive?”; here a ten-vertex counterexample is formally verified in Lean. The classical Tutte 12-cage also refutes the conjecture, as noted in the file; priority for the explicit refutation remains unverified.
CFR525.lean - An affirmative answer to the CFR(5,25) open instance listed by Rosin’s CPro1 (2025), originating from the Handbook of Combinatorial Designs, §VI.62: “Does a 5 × 25 circular Florentine rectangle exist?” Here an explicit witness is formally verified in Lean, proving F_c(25) ≥ 5. This resolves the existence instance, not the exact value of F_c(25).
Pending formalizations:
- Chizewer, Everett, Mithal, and Qiao (2026) [https://arxiv.org/html/2603.27128v1] — Open Problem 4: “Can average-case polynomial-time algorithms be devised for tensor orthogonal and unitary isomorphism over finite fields?”; also Li, Li, Qiao, Tao, and Wang (2026) [https://arxiv.org/html/2604.00591v1] — Problem 1.8: “Can average-case polynomial-time algorithms be devised for 3-tensor isomorphism over finite fields under orthogonal and unitary group actions?” — Here answered affirmatively for cubical tensors under the standard matrix-isometry actions.