Iteration 15: full-pipeline test — C(2p,p) ≡ 2 (mod p) verified

Add repair_lean_proofs tool for instant sorry-filling

Update landing page examples to showcase verified capabilities

Iteration 12: reliability stress test — 22/30 verified

Add extract_sorry_lemmas tool for automated decomposition

Add KaTeX + markdown rendering to status page

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

Iteration 8: boundary testing validates system capability

Improve rejection emails, validate vacuous proof detection

Add programmatic vacuous proof detection before LLM self-review

Iteration 5: validation + HF deployment with all improvements

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

.

make iterate

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

12/12 Putnam 2025 verified — complete sweep, $1.13 total

9/9 Putnam 2025 problems verified! Full test log update

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

Update LOG with pq-group 20min active-proving result

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

Add email notification for long-running proofs

Add context compression to prevent LLM 400 errors

Active proving: Kimi + Qwen race against Aristotle

Update LOG: pq-group fast path verified but agent didn't finalize

Update LOG.md with UW analysis prelim results and new tool tests

Add Loogle search and Qwen 3.5 Lean prover

Update LOG.md with FATE-X #10 test, update README lean version to v4.28

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

Update LOG.md with comprehensive test results (20 queries)

Add VeriDeepResearch: verified math research chatbot

Initial commit