claude-bot
  • Joined on 2026-09-16
claude-bot pushed to main at Zayden-Jung/lean-bench 2026-09-19 19:11:06 +00:00
910633ecb1 Say when the persistent container is running an older image than the build
claude-bot pushed to main at Zayden-Jung/lean-bench 2026-09-19 19:09:17 +00:00
bd26e9ce6e Stop an empty env var from shadowing .env, and refuse a total OCR blackout
claude-bot pushed to main at Zayden-Jung/lean-bench 2026-09-19 16:22:12 +00:00
598f7fd662 Rebuild lean-bench: pages in, verified indexed Lean out
claude-bot pushed to main at Zayden-Jung/lean-bench 2026-09-19 12:28:32 +00:00
0a20042d93 Rebuild lean-bench: pages in, verified indexed Lean out
claude-bot pushed to main at Zayden-Jung/lean-bench 2026-09-19 11:50:58 +00:00
47127aff2e Rebuild lean-bench: pages in, verified indexed Lean out
claude-bot pushed to main at Zayden-Jung/lean-bench 2026-09-19 08:27:56 +00:00
c20121ebe4 Rebuild lean-bench: pages in, verified indexed Lean out
claude-bot pushed to main at Zayden-Jung/lean-bench 2026-09-19 07:16:43 +00:00
b9e37952e6 Rebuild lean-bench: pages in, verified indexed Lean out
claude-bot pushed to main at Zayden-Jung/lean-bench 2026-09-19 07:06:06 +00:00
d3555d9a52 Rebuild lean-bench: pages in, verified indexed Lean out
claude-bot pushed to main at Zayden-Jung/lean-bench 2026-09-18 19:50:13 +00:00
9e0457a0e1 Drop the generated search index; derive it from the source instead
claude-bot pushed to main at Zayden-Jung/lean-bench 2026-09-18 19:43:58 +00:00
fbcb0c3383 Record and gate proofs, so "proven" means Lean verified it
claude-bot pushed to main at Zayden-Jung/lean-bench 2026-09-18 19:36:22 +00:00
69c5b788b9 Generate the citable premise database, and goal-driven retrieval over it
claude-bot pushed to main at Zayden-Jung/lean-bench 2026-09-18 19:27:43 +00:00
04d827b3b3 Split pipeline into real bench (exercises) vs library candidates (body)
claude-bot pushed to main at Zayden-Jung/lean-bench 2026-09-18 17:03:11 +00:00
5aa048593c Note goodman-1.6 dataset now fully elaborates (test push)
claude-bot pushed to main at Zayden-Jung/lean-bench 2026-09-18 16:50:41 +00:00
79c728567a Fix 10 failing goodman-1.6 statements based on Lean compiler diagnostics
claude-bot pushed to main at Zayden-Jung/lean-bench 2026-09-17 17:11:48 +00:00
f98cb41f72 Run textbook pipeline pilot on section 1.6 (Divisibility in the Integers)
claude-bot pushed to main at Zayden-Jung/lean-bench 2026-09-17 17:04:25 +00:00
caedf2e6f4 Add textbook formalization pipeline (extract -> LLM formalize -> elaboration check -> library assembly)