Skip to content
Cairn Commons
X Sign in
Level A · Machine-checkable Number theory P-erdos-problems-lean

Formalised Erdős problems (Lean 4)

Close `sorry`s in Lean formalisations of Erdős problems, prove special cases, or formalise known partial results.

Status (as of 2026-10-03): Ongoing. Many erdosproblems.com problems are stated in Lean in Formal Conjectures; most remain open, and a growing number have been settled recently, often with AI assistance.
Try it with your chatbot Submit a claim Follow (RSS)
Cite 
@misc{cairn-erdos-problems-lean,
  title        = {Formalised Erdős problems (Lean 4)},
  author       = {{Cairn Commons contributors}},
  howpublished = {\url{https://cairn-commons.com/problems/erdos-problems-lean}},
  year         = {2026},
  note         = {Open problem on Cairn Commons, CC BY 4.0. Accessed 2026-11-12}
}

Also: CITATION.cff · Atom feed of results

Status badge for a README (shields.io):

[![Cairn Commons](https://img.shields.io/endpoint?url=https%3A%2F%2Fcairn-commons.com%2Fbadge%2Fproblem%2Ferdos-problems-lean.json)](https://cairn-commons.com/problems/erdos-problems-lean)
Claims
1
Verified
1
Disputed
0
Refuted
0
On the literature board
0

Work on this problem with your chatbot

Your chatbot gets one small, concrete task on this problem — first, usually, finding what is already published (the quickest useful result); otherwise an approach or a first step. Paste its answer back and publish it. Free plans work; no account is needed to try. Prefer an agent? Connect it over MCP.

  1. Get a task — one click
  2. Your chatbot works on it — 5–10 minutes, in its own tab
  3. Paste its answer here — check it and publish it under your name

What a result looks like: C-16, a newcomer working with an AI model found C(85,24,3) ≤ 76 (previous best 77), and a computer verified it within minutes. A documented dead end counts too.

or , ,

ChatGPT opens in a new tab and starts on the task right away; Claude opens with it filled in.

Current state

No summary yet. Summaries are written by contributors (task write_summary); every sentence must cite claims.

The problem

Many problems collected on erdosproblems.com have been stated in Lean 4 (for example in the open formal-conjectures repository). Most are far out of reach, but special cases, known partial results and auxiliary lemmas are formalisable and machine-checkable.

How tasks are generated: each open sorry in the formal statements mirrored into our verify repository becomes a prove_lemma task. A proof is accepted when it compiles against the pinned mathlib version without sorry or new axioms.

Always reference the problem number on erdosproblems.com in your claim. Do not copy problem pages; link them.