These are mathematical proofs I have made available with reproducible verification. For each problem, I searched for an existing proof and did not find one in the sources I examined.
Cheon–Wanless Conjecture 20 (Gyires) · Linear Algebra Appl. 403 (2005) 314–342 · DOI 10.1016/j.laa.2005.02.030 · Gyires 1978, zbMATH 0398.15007
For every real doubly stochastic 4×4 matrix A, 128 per(A)² ≥ 3[per(AAᵀ) + per(AᵀA) + 2 per(A²)], with equality exactly when every entry is 1/4. Only the n = 4 case is proved; the conjecture for general n is not addressed.
Verification: Lean with native_decide; also trusts Lean’s compiler and runtime.
Lean 4.28.0 with Mathlib v4.28.0. The 4×4 theorems depend on Lean.ofReduceBool and Lean.trustCompiler in addition to the standard axioms; the finite certificate is also checked by an independent C++ program.
Petrović–Malešević–Banjac Conjecture 1 · J. Math. Inequal. 14 (2020) 1299–1319 · DOI 10.7153/jmi-2020-14-84 · arXiv:1901.08758
The taxicab Erdős–Mordell inequality holds for every nondegenerate triangle, in every orientation, and every strictly interior point, and the coefficient 3/2 is sharp.
Verification: Lean, kernel-checked; standard axioms only.
Lean 4.35.0 with Mathlib v4.35.0; the five audited declarations depend only on propext, Classical.choice, and Quot.sound.
Prior work: An earlier proof is known; see the entry.
OEIS A057923 · conjecture by Robert Israel, August 13, 2017 · sequence by Larry Reeves, October 3, 2000
The greedy bitwise-OR sequence OEIS A057923 satisfies a(n+2) > a(n) for every n ≥ 0, so its even-indexed and odd-indexed subsequences are both strictly increasing. This is Robert Israel's two-step monotonicity conjecture.
Verification: Lean, kernel-checked; standard axioms only.
Lean 4.35.0 using only Lean's standard library (no Mathlib); the audited checks depend only on propext, Classical.choice, and Quot.sound.