Search results

Bishop–Gromov Route B (Jacobi/Riccati, CH21) — full tracking: Level 1 (assemble leg ①) + Level 2 (cited facts)

Status: Open.

#86 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on Jun 16, 2026

Bishop–Gromov: complete via Route A (Bochner) — discharge the two interfaces

Status: Open.

#85 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on Jun 15, 2026

SmoothManifoldsLee 大分支整合：方案讨论（流程 / 自动化流水线 / 评审分配）

Status: Open.

#61 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on Jun 12, 2026

Tier 3: draft docs/AI_COLLAB.md — AI-driven PR conventions

architectureDesign / module organization changesDesign / module organization changes

documentationImprovements or additions to documentationImprovements or additions to documentation

Status: Open.

#56 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 19, 2026

Tier 3: design — IsStationary/IsStable/IsUnstable quantified-Prop vs explicit-g

architectureDesign / module organization changesDesign / module organization changes

questionFurther information is requestedFurther information is requested

Status: Open.

#55 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 19, 2026

Tier 2: split files exceeding 800 LOC into themed sub-modules

architectureDesign / module organization changesDesign / module organization changes

refactorCode restructuring / reorganizationCode restructuring / reorganization

Status: Open.

#54 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 19, 2026

Tier 2: drive shake baseline 38 → 0

refactorCode restructuring / reorganizationCode restructuring / reorganization

tech-debtKnown engineering debt to clean upKnown engineering debt to clean up

Status: Open.

#53 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 19, 2026

Tier 1: add README.md to 20 sub-directories currently lacking one

documentationImprovements or additions to documentationImprovements or additions to documentation

Status: Open.

#52 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 19, 2026

Tier 1: eliminate maxHeartbeats 800000 hack in BundleSectionContinuity.lean

tech-debtKnown engineering debt to clean upKnown engineering debt to clean up

Status: Open.

#51 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 19, 2026

Tier 1: finish strict-defeq workaround removal (~7 sites left after #43)

blocked-upstreamWaiting on Mathlib / Lean upstreamWaiting on Mathlib / Lean upstream

tech-debtKnown engineering debt to clean upKnown engineering debt to clean up

Status: Open.

#50 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 19, 2026

Tier 1: omit hm — replace 'linter.unusedSectionVars false' with surgical omit (22 files)

refactorCode restructuring / reorganizationCode restructuring / reorganization

tech-debtKnown engineering debt to clean upKnown engineering debt to clean up

Status: Open.

#49 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 19, 2026

[Umbrella] Post-cascade engineering sweep — tech-debt cleanup after explicit-g landing

architectureDesign / module organization changesDesign / module organization changes

refactorCode restructuring / reorganizationCode restructuring / reorganization

tech-debtKnown engineering debt to clean upKnown engineering debt to clean up

Status: Open.

#48 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 19, 2026