Probandum
Formal proof search in Lean
Abstract
Probandum performs finite formal-proof searches from operator-approved Research Programs. Each program binds a sourced question, an exact Lean proposition, pinned dependencies, and explicit run limits. A language model proposes proof terms; Lean accepts or rejects them in an isolated verifier. Only content-addressed records with bound verifier evidence and signed publication approval may enter the public archive.
Method
- Question
- Record the source, exact mathematical scope, source-reported status, and intended claim before the run.
- Formalization
- Bind one Lean declaration, its imports, assumptions, source snapshot, and pinned environment.
- Search
- A language model proposes proof terms. Every response is treated as untrusted input.
- Verification
- A disposable verifier checks the exact candidate against the bound statement and environment.
- Release
- Human approval and inclusion in a signed release snapshot are required before a record becomes public.
Verification
Kernel acceptance means that the exact proof term has the exact formal type in the recorded Lean environment. Each released artifact binds the statement, proof, toolchain, source revision, and verifier evidence.
Informal meaning, novelty, significance, and peer review are separate questions. None is inferred from Lean acceptance.
Verification details