From 2e959f2020bd6e5a77f333369eb3834983449804 Mon Sep 17 00:00:00 2001 From: blfang Date: Thu, 1 Oct 2026 13:09:12 -0400 Subject: [PATCH] Clarify roadmap template prompts Reword each section's prompt as a short question and give every design-decision item a one-sentence description. Co-Authored-By: Claude Opus 5.5 --- roadmap/README.md | 38 +++++++++++++++++++------------------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/roadmap/README.md b/roadmap/README.md index 2b9f3ec..65af253 100644 --- a/roadmap/README.md +++ b/roadmap/README.md @@ -1,35 +1,35 @@ -Proposed road map structure: +Proposed roadmap structure: # Roadmap: topic -## 1. Goal: eventually, what is your goal? Why is it important? +## 1. Goal +What is your goal? Why is it important? -## 2. Completion criterion: -what is the theorem you are viewing as a milestone? -Note the theorem could be big and could be small. +## 2. Completion criteria +Which theorem (big or small) marks this roadmap as done? ## 3. Scope -list the things inside this design doc +What definitions and results will you formalize? + ## 4. Out of scope -what will not be covered -## 5. Mathematical model +What related topics will you leave out, and why? -what is the realtionship between math informally and the thing formally you wanna build +## 5. Mathematical model +What informal math (paper or textbook) are you formalizing, and how does your Lean version differ from it? ## 6. Design decisions and conventions -Lets fix some design choices, choose the choice related to you goal -- carrier types: what is the type of the object you wanna study -- namespace -- parameter order: what are the orders of the object you wanna approach -- totalization/boundary behavior: any potential junk value? -- composition convention -- typeclass assumptions -- finite/infinite conventions +Fix some design choices (select items below that are applicable to your goal): +- Carrier type: what Lean type represents the object you study (e.g. a plain function, a structure, a measure)? +- Namespace: which namespace will your definitions and lemmas live in? +- Parameter order: in what order does each definition take its arguments, given that this fixes what can be partially applied? +- Totalization/boundary behavior: what do your functions return where the math is undefined (junk values such as `x / 0 = 0`)? +- Composition convention: if your objects compose, what does `f.comp g` mean and in which order does it apply? +- Typeclass assumptions: what minimal structure (e.g. `[MeasurableSpace Ω]`, `[Fintype ι]`) does each definition or theorem require? +- Finite/infinite conventions: do you assume finite or general settings (sums vs. integrals, `ℝ` vs. `ℝ≥0∞`/`EReal`)? ## 7. Existing Mathlib and Statlib foundations - -List which PR/file you might be mainly use; also state what willl not be use +Which files or PRs will you build on, and which related ones will you not use? ## 8. Proposed file organization