Mission Control
Lean solver, ShinkaEvolve sessions, and cluster status
Lean Solver
UNKNOWN
Lean 4.29 + Docker
ShinkaEvolve
0
Running Sessions
Compute
fal.ai
Serverless GPU
Intelligence
Gemini
via OpenRouter
LLM Router
OR
OpenRouter API
Lean 4 Proof Checker
Enter Lean 4 code and verify against the theorem prover. Local: lean 4.29.0 | Production: fal.ai serverless Docker
ShinkaEvolve Discovery Sessions
Evolutionary proof discovery powered by LLMs via OpenRouter. Evolves Lean 4 proof tactics to maximize theorems proved.
No sessions running.
Launch a session to start automated Lean 4 proof discovery.
System Architecture
Lean 4 Solver
- Local:
lean 4.29.0via elan - Docker:
leanprovercommunity/lean4 - Production: fal.ai serverless
- Network-isolated, 512MB limit
- 30s timeout per proof
ShinkaEvolve
- LLM + evolutionary algorithms
- OpenRouter: Gemini + Qwen models
- Multi-island population
- 20 Erdos-style theorems
- Baseline: 1/20 → Target: 20/20
Cluster
- Head: Vercel (Next.js 16)
- Compute: fal.ai serverless
- LLMs: OpenRouter multi-model
- Intelligence: Gemini 2.5 Flash
- Data: teorth/erdosproblems live