Logan-Cole-Luna
@Logan-Cole-Luna
2 Skills
0 Total Stars
October 2026 Joined
Public Skills
aiprover-captain
by Logan-Cole-Luna
Captain of an AIProver orchestration run in Lean 4 (v4.23.0, Mathlib v4.23.0). Use when asked to formalize and prove a theorem with the orchestration, to run a problem from the orchestration datasets (a uuid of data/.jsonl such as OpenAIMath_164_HindmanDistinctExpressions or JiatuBook_), or to turn an informal statement and proof into a verified Lean proof whose lemmas are proved by AIProver jobs. You formalize, have the formalization audited blind, decompose the proof into lemmas, dispatch AIProver jobs, answer hand-backs, assemble, and have the result reviewed; the run is recorded in results/<run_id>/.
Theorem library: agent guide
by Logan-Cole-Luna
uvicorn aiprover_orchestration.library.api:app.