Vibe proofs

These are proofs I got from AI/SI in various experiments. Some came from several agents working continuously for many hours. I think this information might be valuable, so I decided to share it publicly rather than keep it on my computer. Some are polished and some are raw drafts.

How to cite: P. Ivanisvili, title, day/month/year, https://paatai.github.io/ai-proofs/#n

verified

the proof has been checked and verified

refereed

an independent AI/SI referee or auditor rated the proof valid

partial result

the note says what is proved and what is open

raw draft

has not been refereed

polished

I partly edited the draft

Lean

the main theorem is formally verified in Lean 4

27 entries, newest first

27. 27 A full solution of the Keller–Klein conjecture: a simplified proof and a complete Lean formalization Nov 9, 2026 raw draft Lean Proves the full Keller–Klein conjecture for every normalized Rademacher sum: if a≥max |a_j|, then both |P(X≤x)−Φ(x)| and |P(X<x)−Φ(x)| are at most Φ(a)−1/2 for every real x. The Lean 4 theorem KellerKlein.keller_klein states both bounds and uses no sorry; the project has 128 Lean files. [PDF · TeX · Lean formalization]
26. 26 Simplified Proof of AA Conjecture after Physical Superintelligence raw draft A three-page simplified proof building on the approach of D. Turturean (Physical Superintelligence). [PDF]
25. 25 A short proof that the Boolean Bohnenblust–Hille constant is at most d²(log d)^3/2+o(1) Nov 6, 2026 refereed BH(d) ≤ C d²(1+log d)^3/2 λ(d)^3/2(1+log λ(d))^1/4, where λ(d)=1+log(1+log d), and also BH(d) ≤ C d²(1+log d)² λ(d)^1/4. The power of d remains 2. The argument is written out in the note. Independent AI audits of that argument found no gap. [PDF · TeX]
24. 24 On the Aaronson–Ambainis conjecture: a quasi-polynomial bound Nov 6, 2026 refereed MaxInf(f) ≥ (Var f/d)^{O(log d)}·exp(−O(log⁴ d)) for every Boolean f of degree d (Theorem 10.1). Written-up proof; the integrated notes and paper text were independently audited. [PDF]
23. 23 The Maurey–Pisier problem for Bourgain–Milman–Wolfson type Nov 3, 2026 verified For every p∈(1,2), a metric space with supremal BMW type exponent p into which the discrete ℓ_p cubes do not embed with uniformly bounded distortion, a negative answer to the Maurey–Pisier problem for BMW type; also an exact characterization of the metric spaces that contain these cubes uniformly. Obtained by Nika Areshidze. [PDF]
22. 22 A comparison inequality for Gaussian vectors and product functions Oct 28, 2026 partial result Sufficient conditions for the comparison inequality are refereed; in an explicit example the exact threshold is open on [2.175…, 2.1925). [PDF · TeX · code]
21. 21 Correlated forward hypercontractivity with outer exponent α<1 Oct 28, 2026 refereed With equal parameters and equal exponents p≥1, the Ivanisvili–Kalantzopoulos covariance condition is necessary and sufficient for every α∈(0,1). With unequal parameters it is not sufficient for r=αp>2; whether it is sufficient for r∈(0,2]∖{1} is open. [PDF · TeX · code]
20. 20 A non-degenerate Gaussian kernel without Gaussian maximisers: Lieb’s formula fails below the diagonal Oct 28, 2026 refereed An Arb-certified counterexample to Lieb’s formula below the diagonal (p>q, genuinely complex case): for the Mehler transform with z=0.72e^0.7i from L^p to L⁴, p≥16, every Gaussian satisfies the inequality but a unimodular function violates it. Rated valid by an independent referee. [PDF · TeX · code]
19. 19 Complex hypercontractivity for several correlated Gaussian functions below the diagonal Oct 28, 2026 raw draft Three parts: an exact criterion for imaginary parameters and every outer exponent; the exact imaginary-axis region for two ρ-correlated functions; and joint narrow-bump counterexamples for general complex z, with two failure points certified in ball arithmetic. Not refereed; off the axes only inner and outer bounds are proved, the region between them is open, and the remaining numerical facts are stated only as evidence. [PDF · code]
18. 18 The local neighborliness threshold of the symmetric moment curve, and the Barvinok–Lee–Novik conjecture for k≤440 and all sufficiently large k Oct 27, 2026 raw draft Not refereed; the conjecture for intermediate k is open. [PDF · TeX]
17. 17 On the Améndola–Lee–Meroni conjecture: the signature volume formula on all subpaths does not characterize cyclic curves Oct 27, 2026 raw draft Claims a counterexample to the conjecture. Not refereed. [PDF · TeX]
16. 16 Carathéodory numbers of the Barvinok–Novik orbitopes, of all four-dimensional SO(2)-orbitopes, and of a further family Oct 27, 2026 raw draft Not refereed. [PDF · TeX]
15. 15 The exact Rosenthal bound for independent zero-mean summands when 3≤p≤4, and in the two extreme regimes when 4<p<5 Oct 26, 2026 partial result Independent adversarial referee passes found no critical or major issues; the middle regime of 4<p<5 is open. [PDF · source and numerics]
14. 14 No 421 equiangular lines in R⁴⁴, no 94 in R²⁰, no 74 in R¹⁹ and no 59 in R¹⁸ Oct 24, 2026 partial result N(44)≤420 and N(20)≤93 are rated valid by an independent auditor and a referee; N(19)≤73 and N(18)≤58 have not been refereed yet. [PDF · TeX · code]
13. 13 Sharp L¹ Poincaré inequality on the Hamming cube Oct 23, 2026 polished An explanation of the proof, based on Tomar’s preprint. [PDF]
12. 12 A sharp reverse Khinchin-type inequality for biased bits: the optimal constant R(q) for every q∈(0,1) Oct 22, 2026 refereed Lean Computer-assisted; rated valid by an independent referee and an auditor. Several agents worked on it over several days. The original output was 192 pages long. Theorem 1.1 is formalized in Lean 4: for every q∈(0,1), the best constant R(q) in E|∑α_iχ_i| ≤ R(q)‖α‖₂, with χ_i=(X_i−q)/√(q(1−q)) for i.i.d. X_i∼Bernoulli(q), is 2√(q(1−q)) max_k≥1 √k max(q,1−q)^k−1, attained by equal coefficients on k=⌊1/(p(2−p))⌋ coordinates, p=min(q,1−q). The Lean theorem ReverseKhinchin.mainTheorem states all of Theorem 1.1 and uses only the standard axioms propext, Classical.choice and Quot.sound; the Lean kernel checks every certificate. The 823 Lean files have about 534,000 lines: 508,000 (720 files) of machine-generated certificate data and 26,000 (103 files) of proof code. An independent referee rated the formalization valid after building it from source with Lean v4.35.0 and re-checking it with the external checker nanoda, except for the certificate computations, which a second checker re-checked on a random sample of 16 certificate modules. Not formalized: Theorem 10.1 and the characterization of the equality cases; Theorems 13.11 and 14.1 are replaced by one statement with new certificates, and Theorem 15.1 is proved with 8551/10000 in place of 171/200, so the formalization should be cited for Theorem 1.1 only. [PDF · proof code · certificates · Lean formalization]
11. 11 List-decoding thresholds of approximate polymorphisms Oct 21, 2026 refereed Shows that a lemma (5.6) in the CFMMS paper is false and that the upper threshold s^U is not tight; rated valid by an independent auditor and a referee. [PDF · numerics]
10. 10 The Keller–Klein Berry–Esseen conjecture: the reachable half for all Rademacher sums, and the full conjecture for a₁≥0.07 Oct 21, 2026 partial result Computer-assisted (ball arithmetic); rated valid by an independent auditor and a referee. The full conjecture for a₁<0.07 remains open. [PDF · certified computation]
9. 9 AND testing with square-root loss: the optimal ε–δ dependence is Θ(√ε), and polynomial bounds for all approximate polymorphisms Oct 21, 2026 refereed Rated valid by an independent auditor and a referee. [PDF · numerics]
8. 8 Ball’s integral inequality via weighted level sets Oct 21, 2026 refereed A short new proof of K. Ball’s 1986 inequality for ∫|sin t / t|^s, s≥2; rated valid by an independent auditor. [PDF · one-page version]
7. 7 The sin-omial integral: a one-page elementary proof Oct 21, 2026 refereed Two short proofs of (1/π)∫₀^π sin^rx / (sin^s(sx/r) sin^r−s((r−s)x/r)) dx = binom(r,s); both rated valid by an independent auditor. [PDF · second proof · audit]
6. 6 The Sánchez-Ruiz entropy bound for all harmonic-oscillator eigenstates: a proof of his Eqs. (30) and (37) Oct 19, 2026 refereed Proof of Eq. (37) of Sánchez-Ruiz (1997); rated valid by an independent auditor. [PDF]
5. 5 Short, computer-free proofs of three nonlinear-mean inequalities of Nazarov, Vasyunin and Volberg Oct 15, 2026 refereed Hand proofs of the I3, I4 and I6 inequalities of arXiv:2204.01336; an independent hostile audit found no errors. [PDF · longer version]
4. 4 Counterexample to Sedykh and Shapiro conjecture Oct 2, 2026 refereed Written-up counterexample. [PDF]
3. 3 Sharp linear hypercontractivity for ultraspherical measures Oct 2, 2026 polished Written-up proof. [PDF]
2. 2 An explicit Bellman function for disjoint partitions: the sharp logarithmic gain for three families Sep 23, 2026 polished Written-up proof with verification code. [PDF · TeX · verification code]
1. 1 Sharp Markov–Bernstein inequality in Gauss space for p≥2 Sep 18, 2026 polished Written-up proof. Prompted and discussed together with Alexandros Eskenazis. [PDF]