Add theorem-question alignment check + honest VERIFIED disclaimer

Add repair_lean_proofs tool for instant sorry-filling

Add extract_sorry_lemmas tool for automated decomposition

Rate-limit Aristotle checks, add stuck detection for repeated errors

Add programmatic vacuous proof detection before LLM self-review

Submit to Aristotle early, add Lean error categorization

Strict self-review: extract theorem statements, ignore comments

Remove blocking wait_for_aristotle — 9x proof throughput improvement

Add hard context reset on LLM errors, first iteration log

Add self-review gate, increase iteration limit, prefer Lean-with-sorry for Aristotle

Refactor to FastAPI + background job architecture

Remove Qwen 3.5, fix sorry/theorem validation, markdown emails

Fix sorry detection, explanation generation, add ISSUES.md

Auto-finalize on verified proof — pq-group solved in 3m23s

Add stats to email: time, cost, tokens, tool call counts

Email now includes proof.lean and research_log.md attachments

Fix examples format, strengthen no-idle prompt, fix email deploy

Add context compression to prevent LLM 400 errors

Active proving: Kimi + Qwen race against Aristotle

Add Loogle search and Qwen 3.5 Lean prover

Improve false-statement handling, increase Aristotle timeout to 2h, better visibility

Add VeriDeepResearch: verified math research chatbot