Pipeline active — accepting submissions

Conjecture Prover

Submit a mathematical conjecture in plain language. Get back a machine-verified Lean 4 proof — or a formal counterexample.

Submit a conjecture View leaderboard

Outcomes

What you get back

Every submission receives a response. The pipeline attempts proof, disproof, and empirical analysis.

Proved

A Lean 4 proof file, LaTeX paper, and PDF — fully machine-verified against Mathlib.

Disproved

A formal counterexample or negation proof with a detailed explanation.

Open

The formal Lean 4 statement plus numerical experiments supporting or refuting your conjecture.

Always

You hear back on every submission — with results, artifacts, and a full report.

Pipeline

How it works

Multiple AI models collaborate to prove your conjecture, with iterative repair and multi-layer verification.

Your conjecture

NL proof sketch

Multi-model debate

Lean 4 formalization

Verify & repair

Semantic & negation guard

Results emailed

Example

What to submit

Sample input

“For every integer n, n⁵ − n is divisible by 30.”

Plain text, LaTeX notation ( $\sum_{k=1}^{n}$ ), or a mix. The more precise your statement, the better the result.

Submit

Your conjecture

State your conjecture as precisely as you can. We'll attempt a formal proof and email you the results.

Your name

Email* — we'll send results here

Conjecture* — state it as precisely as you can

Additional context — background, motivation, known partial results

References — papers, URLs, or textbook citations

Supporting document — optional file with proofs, definitions, or background (max 20 MB)

Results

Conjecture Leaderboard

All submitted conjectures and their verification status. Proved conjectures include a link to the formal proof report.

#	Conjecture	Status	Date
50	AdaBoost Always Cycles? (Global Dynamics Conjecture) Let 𝑆 = { ( 𝑥 𝑖 , 𝑦 𝑖 ) } 𝑖 = 1 𝑚 S={(x i ,y i )} i=1 m be a fixed binary-labeled dataset with 𝑦 𝑖 ∈ { − 1 , + ...	Open — Inconclusive [PDF]	2026-04-25
48	Can Single-Shuffle SGD be Better than Reshuffling SGD and GD? Let n >= 2, K >= 1, and d >= 1. Let S_n denote the set of all permutations of {1,...,n}. For real symmetric d x d mat...	Open — Empirically Refuted [PDF]	2026-04-25
47	Smoothed Complexity of the Simplex Method Fix integers 𝑛 ≥ 1 n≥1 (variables) and 𝑚 ≥ 𝑛 m≥n (constraints). Consider linear programs max ⁡ 𝑥 ∈ 𝑅 𝑛 𝑐 ⊤ 𝑥 subject ...	Open — Empirically Supported [PDF]	2026-04-25
46	Anytime Convergence Rate of Gradient Descent Let 𝑓 : 𝑅 𝑑 → 𝑅 f:R d →R be a convex differentiable function with 𝐿 L-Lipschitz gradient (" 𝐿 L-smooth"), i.e., ∥ ∇ 𝑓...	Open — Inconclusive [PDF]	2026-04-25
45	KLS Conjecture (Kannan–Lovász–Simonovits) For each integer 𝑛 ≥ 1 n≥1, let 𝜇 μ be a Borel probability measure on 𝑅 𝑛 R n that is absolutely continuous with resp...	Open — Empirically Supported [PDF]	2026-04-25
51	Battery Inventory MDP — Optimal Base-Stock Policy Consider a finite-horizon battery operation problem modeled as a stochastic inventory system. Setup. A battery w...	Open — Empirically Supported [PDF]	2026-04-25
44	Let $G \sim G(n, c/n)$ be an Erd\H{o}s--R\'{e}nyi random graph with mean degr... \begin{definition}[Bonacich centrality] For $\beta < \rho(A_S)^{-1}$, the \emph{Bonacich centrality} of node $i \in S...	Open — Inconclusive [PDF]	2026-04-25
43	Every odd integer greater than 5 can be expressed as the sum of a prime and t... Every odd integer greater than 5 can be expressed as the sum of a prime and twice another prime.	Open — Empirically Supported [PDF]	2026-04-25
40	Let A be subset of the set {1,...,N} such that there is no solution to at = b... Let A be subset of the set {1,...,N} such that there is no solution to at = b where a,b in A and the smallest prime f...	Open — Empirically Supported [PDF]	2026-04-25
39	A unitary divisor d of a positive integer n is a divisor such that d and n/d ... A unitary divisor d of a positive integer n is a divisor such that d and n/d are coprime. A positive integer n is cal...	Open — Empirically Supported [PDF]	2026-04-25
36	Let n be a positive integer and define L_n to be the least common multiple of... Let n be a positive integer and define L_n to be the least common multiple of {1,...,n} and define a_n such that a_n ...	Open — Empirically Supported [PDF]	2026-04-24
24	Let n be a positive integer and define L_n to be the least common multiple of... Let n be a positive integer and define L_n to be the least common multiple of {1,...,n} and define a_n such that a_n ...	Open — Empirically Supported [PDF]	2026-04-23
10	Every odd integer greater than 5 can be expressed as the sum of a prime and t... Every odd integer greater than 5 can be expressed as the sum of a prime and twice another prime.	Open — Empirically Supported [PDF]	2026-04-22
31	Let $G \sim G(n, c/n)$ be an Erd\H{o}s--R\'{e}nyi random graph with mean degr... \begin{definition}[Bonacich centrality] For $\beta < \rho(A_S)^{-1}$, the \emph{Bonacich centrality} of node $i \in S...	Open — Empirically Supported [PDF]	2026-04-21
29	AdaBoost Always Cycles? (Global Dynamics Conjecture) Let 𝑆 = { ( 𝑥 𝑖 , 𝑦 𝑖 ) } 𝑖 = 1 𝑚 S={(x i ,y i )} i=1 m be a fixed binary-labeled dataset with 𝑦 𝑖 ∈ { − 1 , + ...	Open — Inconclusive [PDF]	2026-04-21
21	If A is a subset of the natural numbers such that the sum of the reciprocals ... If A is a subset of the natural numbers such that the sum of the reciprocals of the elements in A is infinite, then A...	Open — Empirically Supported [PDF]	2026-04-21
27	Smoothed Complexity of the Simplex Method Fix integers 𝑛 ≥ 1 n≥1 (variables) and 𝑚 ≥ 𝑛 m≥n (constraints). Consider linear programs max ⁡ 𝑥 ∈ 𝑅 𝑛 𝑐 ⊤ 𝑥 subject ...	Formally Disproved [PDF]	2026-04-21
13	The Kerr black hole metric is stable, in the sens that small perturbations of... The Kerr black hole metric is stable, in the sens that small perturbations of the initial data leads to a solution wh...	Open — Empirically Supported [PDF]	2026-04-21
8	If statement P implies statement Q, and statement P is true, then statement Q... If statement P implies statement Q, and statement P is true, then statement Q must also be true.	Formally Proved [PDF]	2026-04-21
16	Anytime Convergence Rate of Gradient Descent Let 𝑓 : 𝑅 𝑑 → 𝑅 f:R d →R be a convex differentiable function with 𝐿 L-Lipschitz gradient (" 𝐿 L-smooth"), i.e., ∥ ∇ 𝑓...	Open — Empirically Supported [PDF]	2026-04-21
18	Can Single-Shuffle SGD be Better than Reshuffling SGD and GD? Let n >= 2, K >= 1, and d >= 1. Let S_n denote the set of all permutations of {1,...,n}. For real symmetric d x d mat...	Open — Empirically Supported [PDF]	2026-04-21
20	Can Single-Shuffle SGD be Better than Reshuffling SGD and GD? Let n >= 2, K >= 1, and d >= 1. Let S_n denote the set of all permutations of {1,...,n}. For real symmetric d x d mat...	Open — Empirically Supported [PDF]	2026-04-21
12	```Research Proposal: Asymptotic Consistency & Scaling Laws for Reference-Fre... by Brando Miranda, Henry Bosch, et al. Summary We propose establishing the theoretical foundations of Total Variation...	Open — Inconclusive [PDF]	2026-04-21
19	Smoothed Complexity of the Simplex Method Fix integers 𝑛 ≥ 1 n≥1 (variables) and 𝑚 ≥ 𝑛 m≥n (constraints). Consider linear programs max ⁡ 𝑥 ∈ 𝑅 𝑛 𝑐 ⊤ 𝑥 subject ...	Formally Disproved [PDF]	2026-04-21
3	Every even integer strictly greater than 2 can be expressed as the sum of two... Every even integer strictly greater than 2 can be expressed as the sum of two prime numbers.	Open — Inconclusive [PDF]	2026-04-21
1	a^2 + b2 = c^2 (pythagoras) a^2 + b2 = c^2 (pythagoras)	Formally Proved [PDF]	2026-04-21
17	Smoothed Complexity of the Simplex Method Fix integers 𝑛 ≥ 1 n≥1 (variables) and 𝑚 ≥ 𝑛 m≥n (constraints). Consider linear programs max ⁡ 𝑥 ∈ 𝑅 𝑛 𝑐 ⊤ 𝑥 subject ...	Open — Empirically Supported [PDF]	2026-04-21
14	KLS Conjecture (Kannan–Lovász–Simonovits) For each integer 𝑛 ≥ 1 n≥1, let 𝜇 μ be a Borel probability measure on 𝑅 𝑛 R n that is absolutely continuous with resp...	Open — Empirically Supported [PDF]	2026-04-21
5	There are infinitely many pairs of prime numbers that differ by exactly 2. There are infinitely many pairs of prime numbers that differ by exactly 2.	Open — Inconclusive [PDF]	2026-04-21
15	AdaBoost Always Cycles? (Global Dynamics Conjecture) Let 𝑆 = { ( 𝑥 𝑖 , 𝑦 𝑖 ) } 𝑖 = 1 𝑚 S={(x i ,y i )} i=1 m be a fixed binary-labeled dataset with 𝑦 𝑖 ∈ { − 1 , + ...	Formally Disproved [PDF]	2026-04-21
25	Let A be subset of the set {1,...,N} such that there is no solution to at = b... Let A be subset of the set {1,...,N} such that there is no solution to at = b where a,b in A and the smallest prime f...	Open — Empirically Supported [PDF]	2026-04-21
22	Let A be a set of positive integers. For each n in A, choose some collection ... Let A be a set of positive integers. For each n in A, choose some collection X_n of forbidden residue classes modulo...	Open — Inconclusive [PDF]	2026-04-21
9	The Riemann zeta function evaluated at −1 equals −1/12. The Riemann zeta function evaluated at −1 equals −1/12.	Formally Proved [PDF]	2026-04-21
23	A unitary divisor d of a positive integer n is a divisor such that d and n/d ... A unitary divisor d of a positive integer n is a divisor such that d and n/d are coprime. A positive integer n is cal...	Open — Empirically Supported [PDF]	2026-04-21
11	Let $G \sim G(n, c/n)$ be an Erd\H{o}s--R\'{e}nyi random graph with mean degr... \begin{definition}[Bonacich centrality] For $\beta < \rho(A_S)^{-1}$, the \emph{Bonacich centrality} of node $i \in S...	Open — Inconclusive [PDF]	2026-04-21
2	Any number divided by itself is a whole number Any number divided by itself is a whole number	Formally Disproved [PDF]	2026-04-20
26	Let A be an infinite subset which contains no three points on a line and no f... Let A be an infinite subset which contains no three points on a line and no four points on a circle. Consider the gra...	Formally Disproved [PDF]	2026-04-20
4	The sum of the first n odd natural numbers equals n^2 The sum of the first n odd natural numbers equals n^2	Formally Proved [PDF]	2026-04-20
6	There are no two integers a and b (where b is not zero) such that the fractio... There are no two integers a and b (where b is not zero) such that the fraction a/b squared equals 2.	Formally Proved [PDF]	2026-04-20
7	For every integer n, n^5− n is divisible by 30 For every integer n, n^5− n is divisible by 30	Formally Proved [PDF]	2026-04-20