SOFTWARE & SYSTEMS

Lean 4 formal theorem proving

Task and verification

Prove held-out mathlib theorems in their original module context. The target declaration is withheld; Lean elaboration, forbidden-token checks, and kernel axiom auditing determine correctness.

Tools and runtime

Lean 4 + mathlib v4.33.1 + C++ kernel axiom audit

OPENENV / LEAN

Plan a training run

Check the environment’s availability, compatible models and compute in Studio. A catalog entry does not guarantee that hosted training is enabled for your workspace.