Skip to content

Pull requests: rjwalters/lean-genius

New pull request New
18 Open 20,528 Closed
18 Open 20,528 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

fix(meta): circumference-via-differentiation-oq-03 lineCount 93→152
#21530 opened May 31, 2026 by rjwalters Owner Loading…
Research: minkowski-theorem-oq-02-oq-03 — S13 S6 ACT simultaneous_dirichlet_from_minkowski (OQ-03 graduation candidate, build pending — G9 lake self-loop) research Research agent work
#21529 opened May 31, 2026 by rjwalters Owner Loading…
3 tasks
fix(meta): ballot-problem-oq-03-oq-02 lineCount 2532→2528
#21528 opened May 31, 2026 by rjwalters Owner Loading…
fix(meta): descartes-rule-of-signs-oq-02-oq-01-oq-02 lineCount 458→533
#21527 opened May 31, 2026 by rjwalters Owner Loading…
fix(meta): borsuk-ulam-oq-02-oq-01-oq-03-oq-02 lineCount 1788→1885
#21526 opened May 31, 2026 by rjwalters Owner Loading…
audit(erdos-161): mark clean cycle 5
#21521 opened May 31, 2026 by rjwalters Owner Loading…
4 tasks done
audit(erdos-161): mark clean (cycle 4)
#21516 opened May 31, 2026 by rjwalters Owner Loading…
4 tasks done
audit(erdos-161): mark clean (cycle 4) — F^(t)(n,α) jump axiomatization integrity verified
#21509 opened May 31, 2026 by rjwalters Owner Loading…
3 tasks done
audit(erdos-162): realign stale section line ranges + tighten function-f summary
#21504 opened May 31, 2026 by rjwalters Owner Loading…
3 of 4 tasks
Enrich abel-ruffini-galois-extensions-oq-05: Jordan-Hoelder + Chebotarev cross-refs enrichment Gallery proof enrichment
#21503 opened May 31, 2026 by rjwalters Owner Loading…
audit(erdos-162): cycle 6 — same issue persists, mechanic PR #21488 still open
#21500 opened May 31, 2026 by rjwalters Owner Loading…
audit(erdos-162): cycle 4 issues-found — section line ranges stale (#21485)
#21487 opened May 31, 2026 by rjwalters Owner Loading…
4 tasks done
audit(erdos-166): mark clean (cycle 5) — R(4,k) Ramsey lower bound integrity verified
#21483 opened May 31, 2026 by rjwalters Owner Loading…
3 tasks done
audit(erdos-166): mark clean (cycle 4) — R(4,k) Ramsey lower bound integrity verified
#21480 opened May 31, 2026 by rjwalters Owner Loading…
4 tasks done
audit(erdos-166): mark clean — R(4,k) Ramsey bound integrity verified
#21476 opened May 31, 2026 by rjwalters Owner Loading…
4 tasks done
research(cantor-diagonalization-oq-01-oq-01-oq-02-oq-01): S6 — Easton-function closure under pointwise binary max (build pending) research Research agent work
#17137 opened May 8, 2026 by rjwalters Owner • Draft
4 tasks
research(cantor-diagonalization-oq-04-oq-01): S2 — trivial setoid + refinement-descent (build pending) research Research agent work
#17030 opened May 8, 2026 by rjwalters Owner • Draft
3 tasks
research(cantor-diagonalization-oq-01-oq-01-oq-02-oq-01): S5 — Easton non-examples + lt_apply corollary research Research agent work
#16936 opened May 8, 2026 by rjwalters Owner • Draft
3 tasks
1
ProTip! Adding no:label will show everything without a label.