PrithwishJana

AIProver — AI skill for Claude Code

AI community

AIProver post-trains an open-weight LLM and evolves its harness from verifier rewards and certificates.

How to install AIProver

This entry records only its repository, not the path inside it, so there is no exact command to give. Open PrithwishJana/AIProver and copy the folder into ~/.claude/skills/, or the file into ~/.claude/agents/.

What AIProver does

AIProver post-trains an open-weight LLM and evolves its harness from verifier rewards and certificates. It outperforms open-weight system at research-level proof auto-formalization, and as a Claude Code/Codex skill beats prior agents at lower cost.

Alternatives in AI

ARIS Agent Guide — For AI agents reading this repo 6.2k ★
Open Multi Agent — TypeScript multi-agent orchestration engine — one runTeam() call from goal to result 5.8k ★
Post Training — ai-research-skills GRPO, RLHF, DPO, SimPO 5.4k ★

README

AIProver

AIProver auto-formalizes a natural-language theorem **and its proof** into a Lean 4 file that compiles, has no `sorry`, states exactly that theorem and follows that proof. It is a fine-tuned Leanstral-class prover driven by an evolved agentic harness (Lean 4.23.0, Mathlib, cslib, the lean-lsp tools), packaged so it can be used in three ways:

mode	what you run	who judges the result
standalone	`bin/aiprover` (submit / wait / result / check / probe / search)	you
Claude Code plugin	Claude Code with the `aiprover-autoformalize` skill	Claude Code: plans, delegates Lean work to AIProver, judges faithfulness, decomposes and weaves
Codex skill	Codex with the same skill	Codex, likewise

Everything lives in [`AIProver_plugin/`](AIProver_plugin/). The model itself runs on a GPU server you point the plugin at; the harness, the Lean toolchain and the tools run on your machine.

How it works

Four parties take part, and the division of labour is fixed: judgement stays with the strongest model available, Lean work goes to the specialist.

party	runs where	does
You	your terminal	supply the theorem and its proof in the two tagged blocks; in standalone mode you are also the judge
Coding agent (Claude Code or Codex, on your own subscription)	your machine	reads the text, rewrites the proof as explicit steps, decides what to delegate, judges every candidate for faithfulness, decomposes, weaves, and gates the final file. Never grinds through tactic search itself
AIProver (the Leanstral-class prover inside its evolved harness)	the GPU server	auto-formalizes a problem into a Lean file: writes, compiles, searches Mathlib and cslib, reads goals and repairs, for up to 200 turns per call. Returns candidates; cannot be trusted to judge its own statement
Mechanical checks (`check`, `probe`, lean-lsp)	your machine	kernel-level compile and completeness, count