mathematica-in-lean

Overview

mathematica-in-lean ports Rob Lewis and Minchao Wu’s Lean 3 Wolfram bridge to Lean 4 and mathlib4, then goes further: instead of just trusting Wolfram’s answers, most of its tactics use Wolfram only to discover a certificate — a polynomial identity, a rewrite step, a Wilf–Zeilberger recurrence — while Lean’s own kernel checks it, so #print axioms stays free of any oracle.

Why and how it was built

The flagship result, ∑ C(n,k)² = C(2n,n), is proved via a certificate Wolfram found and Lean independently verified. It was built with Claude doing the exploratory and mechanical work — porting types, writing tactic plumbing, drafting the telescoping proof — while Matthew set the bar for what counts as done: sorry-free, axiom-clean, kernel-checked. That standard is what’s distinctive here: a CAS proposes, but only the Lean kernel gets to decide.

Key Features

  • Wolfram-assisted tactics that discover certificates; Lean’s kernel independently checks them, so no proof trusts Wolfram’s output directly
  • Ported to Lean 4 / mathlib4 from the original Lean 3 bridge
  • The flagship proof (∑ C(n,k)² = C(2n,n)) is sorry-free and kernel-checked

Status

grep -rn "sorry" --include="*.lean" . across the repo returns zero matches, and lake build Mathematica completes cleanly. The flagship theorem’s axiom list is limited to [propext, Classical.choice, Quot.sound] — no sorry, no trust axiom — genuinely PROVED, not just asserted. examples/Demos.lean and ZeilbergerBridge.lean need a live Wolfram kernel to re-verify and haven’t been independently re-checked recently; treat those as OPEN pending that check, not proved. Not a deployable app — a Lean library, used via Lake.