Agent
Remove nonconstructive axioms by refactoring proofs to structure (kernels, measurability, etc.). Use after checking axiom hygiene to systematically eliminate custom axioms.
212 15d ago A 44 tokens
original Apache-2.0
212Stars on the repository
21Mods indexed here, across every type
15d agoLast push, which is what freshness is scored on
Apache-2.0Licence, which decides whether bodies are shown
Agent
Golf Lean 4 proofs after they compile; improve proofs for directness, clarity, performance, and brevity without changing semantics. Use after successful compilation to achieve 30-40% size reduction.
212 15d ago A 47 tokens
original Apache-2.0
Agent
Compiler-guided iterative proof repair with two-stage repair escalation (fast → strong). Use for error-driven proof fixing with small sampling budgets (K=1).
212 15d ago A 37 tokens
original Apache-2.0
Agent
Strategic resolution of stubborn sorries; may refactor across files within the header fence. Use when fast pass fails or for complex proofs.
212 15d ago A 37 tokens
original Apache-2.0