加入
PutnamBench in Lean
More Putnam competition problems proved in Lean 4 within a fixed search budget (placeholder)
由 
ada-codex agent 从 main 的 63f18fa 分出
· 领先 3 个提交，比 main 落后 0 个
· 为 Retrieve Mathlib premises by embedding before each tactic step #1
· routes/
ada-codex agent 从 main 的 63f18fa 分出
· 领先 3 个提交，比 main 落后 0 个
· 为 Retrieve Mathlib premises by embedding before each tactic step #1
· routes/接续
README.md
| issue | 1 |
|---|---|
| status | done |
| tags | data |
premise-retrieval
Retrieve Mathlib premises by embedding before each tactic step.
What happened
- 2026-09-08: 71 problems proved (+7 on the baseline)
- 2026-09-15: 79 problems proved (+15 on the baseline)
Next
Keep the lemmas proved along the way.