Lean Proof-Search Lab Runtime

Finds tactic scripts the real Lean prover accepts on toy theorems, and refuses proofs that cheat.

Contract

Does A small, runnable proof-search lab for toy logic theorems, checked by the real Lean theorem prover. For each toy theorem it searches over candidate tactic scripts, compiles each one with Lean, and keeps a script only when Lean actually closes the proof. It refuses three ways of cheating: forwarding a ready-made proof body (an oracle leak), leaning on `sorry` or extra axioms (an unclean proof), and a policy that only picks the right tactic because it recognised the problem's name (memorisation, caught by renaming the problem). It shows one honest search succeeding and four cheats being rejected. Lean is optional: install it to unlock the real run; without it the lab reports itself locked and claims nothing, rather than pretending to have proved anything.

Scope limit This standard governs a bounded symbolic Lean proof-search lab over tiny public toy-theorem fixtures whose verdict source is the installed Lean subprocess only. It is not neural theorem proving, does not solve any open mathematical problem, does not forward oracle proof bodies, is not frontier-scale math automation or online-RL bandit search, is not a private source prover-run export, and excludes launch or public sharing.

Run

Quick probe

microcosm lean-proof-search-lab-runtime run --input fixtures/first_wave/lean_proof_search_lab_runtime/input --out /tmp/plectis-public-runs/lean_proof_search_lab_runtime

Validator command

microcosm lean-proof-search-lab-runtime run --input fixtures/first_wave/lean_proof_search_lab_runtime/input --out receipts/first_wave/lean_proof_search_lab_runtime --acceptance-out receipts/acceptance/first_wave/lean_proof_search_lab_runtime_fixture_acceptance.json

Evidence

ClassExternal tool runevidence 4/5Real runtime resultRuns real tools

Links to Certificate Kernel Execution Lab, Verifier Lab Kernel, Formal Math Lean Proof Witness

formal-maththeorem-provingproof-search

Source

Source Design note · Source

Map Show on the map

Index Open compact index card

Paper module

Paper module Lean Proof-Search Lab Runtime

Gated external-tool proof-search lab that searches toy Lean theorems, checks each candidate with the installed Lean subprocess, and rejects oracle leaks, axiom taint, and problem-id memorisation by recomputation; locked and claimless when Lean is absent.

Read the full write-up

Back to Components index → Reference roster →