Last released Oct 18, 2026
Coordinate several agents on a Lean 4 formalization: state derived from the compiled environment, locked statements, recorded claims and memory-guarded jobs