ProofLab

Interactive Neural Theorem Proving & Formal Verification Laboratory β€” Explore how AI proves mathematical theorems through proof search, tactic prediction, and the Curry-Howard correspondence

Proof Tree Explorer

Visualize how automated theorem provers search for proofs: goals split into subgoals via tactics, forming a search tree with backtracking and success paths.

Theorem Selection

Ready

Current Goal State

-- Select a theorem and step through the proof -- Goals appear here as the prover works ⊒ βˆ€ n : β„•, n + 0 = n

Tactic Trace

Statistics

0
Nodes Explored
0
Max Depth
0
Backtracks

Neural Tactic Predictor

Train a miniature neural network to predict the next proof tactic given a goal state β€” the core mechanism behind systems like AlphaProof and LeanDojo.

Training Visualization

Epoch: 0 | Loss: β€”

Loss Curve

Goal β†’ Tactic Predictions

The network maps goal embeddings to tactic probability distributions

Goal: n + 0 = n
Goal: a + b = b + a
Goal: P β†’ (P β†’ Q) β†’ Q

Model Architecture

NeuralTacticPredictor( encoder: Linear(goal_dim=8, hidden=16) activation: ReLU decoder: Linear(hidden=16, tactics=6) output: Softmax ) Tactics: [induction, rewrite, intro, apply, simp, rfl] Training: CrossEntropy + SGD(lr=0.1)

Training Data (Proof Corpus)

-- 12 goalβ†’tactic pairs from Lean4 mathlib {goal: "n+0=n", tactic: "induction"} {goal: "a+b=b+a", tactic: "induction"} {goal: "Pβ†’(Pβ†’Q)β†’Q", tactic: "intro"} {goal: "succ n=succ m", tactic: "simp"} {goal: "0+n=n", tactic: "induction"} {goal: "a*(b+c)=..", tactic: "rewrite"} {goal: "P∧Qβ†’Q∧P", tactic: "intro"} {goal: "n=n", tactic: "rfl"} {goal: "a+succ b=..", tactic: "rewrite"} {goal: "Pβ†’P", tactic: "intro"} {goal: "list.lenβ‰₯0", tactic: "induction"} {goal: "f(g(x))=..", tactic: "simp"}

SAT β†’ Proof Visualizer

Watch the DPLL/CDCL algorithm solve Boolean satisfiability problems step-by-step. See how conflict-driven clause learning creates resolution proofs.

SAT Instance

Decision Trail

-- Assignments will appear here -- D=Decision, P=Propagation, C=Conflict

Learned Clauses

-- Conflict-driven clauses appear here

Statistics

0
Decisions
0
Propagations
0
Conflicts

Curry-Howard Playground

The Curry-Howard correspondence: proofs ARE programs, propositions ARE types. Construct proofs by building Ξ»-terms in a simple type theory.

Proposition to Prove

Type (Proposition):
A β†’ A
Term (Proof):
_

Context (Hypotheses)

-- Available assumptions will appear here

Correspondence Table

LogicProgramming
PropositionType
ProofProgram (term)
A β†’ B (implication)A β†’ B (function)
A ∧ B (conjunction)A Γ— B (product)
A ∨ B (disjunction)A + B (sum)
βˆ€x.P(x)Ξ (x:A).B(x)
βˆƒx.P(x)Ξ£(x:A).B(x)

Proof History

Proof Difficulty Estimator

Neural provers use structural features to estimate theorem difficulty and guide search. Explore how proof complexity correlates with syntactic and semantic features.

Theorem Feature Space

Difficulty Prediction

Feature Importance (Learned Weights)

Difficulty Distribution

Verification Arena

Race neural proof search against classical tactic-based approaches on benchmark theorems. See where AI excels and where traditional methods still win.

NEURAL Neural Proof Search (AlphaProof-style)

Proved: 0/20 Failed: 0 Time: 0.0s

CLASSICAL Classical Tactic Search (BFS + Heuristics)

Proved: 0/20 Failed: 0 Time: 0.0s

Head-to-Head Results

β€”
Neural Wins
β€”
Ties
β€”
Classical Wins