Search results

vite build hangs in dev checkout: Tailwind v4 scans nested worktree repo copies

Status: Open.

#21009 In rjwalters/lean-genius;

· rjwalters opened on May 29, 2026

Build perf phase 3: apply static-data + fetch pattern to research data loader

Status: Open.

#20994 In rjwalters/lean-genius;

· rjwalters opened on May 29, 2026

Build perf phase 2: move meta/annotations to public/, add hashed manifest, delete per-proof shims

Status: Open.

#20993 In rjwalters/lean-genius;

· rjwalters opened on May 29, 2026

Tooling: lint/script to catch in-body namespace-qualified refs after rename

Status: Open.

#20847 In rjwalters/lean-genius;

· rjwalters opened on May 27, 2026

Erdős #138: bridging lemma between ℕ-form and ℤ-form difference statement

epic:erdosErdős Problems EpicErdős Problems Epic

researchResearch agent workResearch agent work

Status: Open.

#20843 In rjwalters/lean-genius;

· rjwalters opened on May 27, 2026

Fill 14 sorry placeholders in Erdos125PositiveLowerDensity.lean

enrichmentGallery proof enrichmentGallery proof enrichment

epic:erdosErdős Problems EpicErdős Problems Epic

researchResearch agent workResearch agent work

Status: Open.

#20842 In rjwalters/lean-genius;

· rjwalters opened on May 27, 2026

Verify AlphaProof Nexus port docker builds (6 unverified PRs)

epic:erdosErdős Problems EpicErdős Problems Epic

researchResearch agent workResearch agent work

Status: Open.

#20841 In rjwalters/lean-genius;

· rjwalters opened on May 27, 2026

Mathlib prerequisites scoping: class field towers and Golod-Shafarevich (follow-up to #20516)

epic:erdosErdős Problems EpicErdős Problems Epic

loom:curatedEnhanced by Curator, awaiting human approvalEnhanced by Curator, awaiting human approval

researchResearch agent workResearch agent work

Status: Open.

#20577 In rjwalters/lean-genius;

· rjwalters opened on May 23, 2026

Lean formalization of OpenAI 2026 unit-distance lower-bound construction (follow-up to #20516)

epic:erdosErdős Problems EpicErdős Problems Epic

loom:triageNew issue awaiting Curator enhancementNew issue awaiting Curator enhancement

researchResearch agent workResearch agent work

Status: Open.

#20576 In rjwalters/lean-genius;

· rjwalters opened on May 23, 2026

Batch-backfill 104 unfilled Seeker stub research entries

loom:curatedEnhanced by Curator, awaiting human approvalEnhanced by Curator, awaiting human approval

Status: Open.

#20253 In rjwalters/lean-genius;

· rjwalters opened on May 17, 2026

Redesign boundary analysis + prove boundary_doors_odd for Sperner grid

loom:blockedImplementation blocked, needs help or clarificationImplementation blocked, needs help or clarification

loom:curatedEnhanced by Curator, awaiting human approvalEnhanced by Curator, awaiting human approval

researchResearch agent workResearch agent work

Status: Open.

#9044 In rjwalters/lean-genius;

· rjwalters opened on Apr 3, 2026

Sperner Part 2: SimplicialComplex → CellComplex bridge for mathlib4#25231

epic:mathlibMathlib Contribution EpicMathlib Contribution Epic

loom:blockedImplementation blocked, needs help or clarificationImplementation blocked, needs help or clarification

loom:curatedEnhanced by Curator, awaiting human approvalEnhanced by Curator, awaiting human approval

researchResearch agent workResearch agent work

Status: Open.

#8998 In rjwalters/lean-genius;

· rjwalters opened on Apr 3, 2026