Open library

Proofs anyone can read.

Every proof here was accepted by the checker: compiled by Lean, replayed through the kernel, resting on the three standard axioms. Read one, learn from it, or hand it to your prover.

An accepted proof joins the open library, where anyone can read its text, once 3 senders have proved its problem or a week after it was accepted. A refused proof stays private. Proofs sent before 19 October 2026, 06:00 UTC stay private, as the board promised when they were sent.