Repository navigation
Expand the packet curriculum taxonomy across mathematics and add a generic first-principles-to-frontier authoring prompt #11
Description
Summary
Expand packets/ into a comprehensive curriculum and research taxonomy covering the major genres, subfields, and methodological lanes of mathematics, then add a reusable authoring prompt for each category that ingests pedagogy, textbooks, surveys, research papers, benchmark statements, and frontier problems and turns them into verifier-gated MathCorpus packets from first principles through the current research frontier.
This should preserve the existing design invariant:
- a packet is one JSON file, not a directory;
- category and subcategory directories organize packets;
- Lean proof bodies live under the matching
lean/MathCorpus/...tree; - proof authority comes only from the pinned verifier;
- literature, pedagogy, model reasoning, and paper claims are inputs and provenance, never proof authority by themselves.
Why this is needed
The current corpus already has the correct concept-packet model, schema, validator, trust ladder, MCIP evidence layer, literature lineage, negative examples, and Proof Search integration. What is missing is a broad, explicit curriculum map that tells authoring agents what packet families must exist in every mathematical genre and how to grow each family from basic definitions to active research.
The goal is not to create empty directories for appearance. The goal is to create a machine-readable research curriculum where every branch has:
- definitions and canonical objects;
- elementary examples and counterexamples;
- core lemmas and proof patterns;
- standard theorems;
- algorithms and certificates where relevant;
- common failed approaches and diagnostics;
- cross-domain dependencies;
- literature lineage and attribution;
- known formalization gaps;
- frontier-aligned theorem and research packets.
Existing architecture to preserve
MathCorpus already defines:
- packets as single JSON concept records;
- levels
L0_elementarythroughL7_frontier; - kinds including concept, theorem, exercise, certificate claim, negative example, benchmark item, and frontier artifact;
- canonical hashes, proof authority, redaction, training eligibility, and provenance;
- MCIP child evidence for proof variants, dependencies, attempts, repairs, model runs, literature lineage, and publication;
- paired Lean modules under
lean/MathCorpus/...; author_packet.py, validation, hashing, export, dedupe, and split tooling.
This issue should extend the taxonomy and authoring process without weakening those controls.
Proposed top-level curriculum tree
The directory names below are category directories containing packet JSON files. They are not per-packet folders.
packets/
elementary/
proof_basics/
olympiad/
undergraduate/
advanced_undergraduate/
graduate/
known_theorems/
frontier/
negative/
benchmarks/
certificates/
algorithms/
cross_domain/
Each level should support a common subject taxonomy, with additional research-specific branches under frontier/.
Comprehensive subject and genre taxonomy
Foundations and logic
logic/
propositional_logic/
predicate_logic/
proof_theory/
model_theory/
computability/
type_theory/
category_theoretic_logic/
constructive_mathematics/
reverse_mathematics/
automated_reasoning/
satisfiability_and_certificates/
set_theory/
elementary_set_theory/
ordinals/
cardinals/
choice_principles/
descriptive_set_theory/
forcing/
large_cardinals/
foundations/
formalization_fidelity/
encoding_soundness/
theorem_statement_normalization/
proof_certificates/
trust_and_replay/
Arithmetic and number theory
arithmetic/
numerals/
divisibility/
gcd_lcm/
modular_arithmetic/
finite_sums_products/
inequalities/
number_theory/
elementary_number_theory/
multiplicative_number_theory/
additive_number_theory/
analytic_number_theory/
algebraic_number_theory/
arithmetic_geometry/
diophantine_equations/
prime_numbers/
sieve_methods/
transcendence/
modular_forms/
elliptic_curves/
computational_number_theory/
cryptographic_number_theory/
Algebra
algebra/
elementary_algebra/
equations_and_inequalities/
polynomials/
rational_functions/
recurrences/
abstract_algebra/
groups/
rings/
fields/
modules/
representation_theory/
commutative_algebra/
homological_algebra/
universal_algebra/
lattice_theory/
semigroups_and_monoids/
computational_algebra/
galois_theory/
lie_theory/
algebraic_geometry/
noncommutative_algebra/
Linear algebra and optimization
linear_algebra/
vectors_and_matrices/
linear_maps/
determinants/
eigenvalues/
bilinear_and_quadratic_forms/
tensor_products/
canonical_forms/
numerical_linear_algebra/
optimization/
linear_programming/
convex_optimization/
integer_programming/
combinatorial_optimization/
semidefinite_programming/
variational_methods/
optimal_transport/
approximation_algorithms/
optimization_certificates/
Combinatorics
combinatorics/
basic_counting/
bijections/
inclusion_exclusion/
generating_functions/
recurrences/
enumerative_combinatorics/
extremal_combinatorics/
probabilistic_combinatorics/
algebraic_combinatorics/
additive_combinatorics/
geometric_combinatorics/
topological_combinatorics/
design_theory/
matroid_theory/
posets_and_lattices/
ramsey_theory/
discrepancy_theory/
coding_theory/
finite_geometry/
combinatorial_species/
experimental_combinatorics/
Graph theory
graph_theory/
graph_foundations/
graph_invariants/
paths_cycles_connectivity/
trees/
matchings_and_factors/
colorings/
domination_and_independence/
extremal_graph_theory/
structural_graph_theory/
forbidden_subgraphs/
planar_graphs/
topological_graph_theory/
algebraic_graph_theory/
spectral_graph_theory/
probabilistic_graph_theory/
random_graphs/
graph_algorithms/
graph_complexity/
parameterized_complexity/
graph_decompositions/
graph_minors/
hypergraphs/
directed_graphs/
signed_and_weighted_graphs/
graph_limits/
network_science_foundations/
conjecture_audits/
certificate_backed_counterexamples/
Analysis
analysis/
limits_and_continuity/
differentiation/
integration/
sequences_and_series/
inequalities/
real_analysis/
measure_theory/
functional_analysis/
harmonic_analysis/
complex_analysis/
fourier_analysis/
operator_theory/
approximation_theory/
special_functions/
asymptotic_analysis/
distribution_theory/
geometric_measure_theory/
Differential equations and dynamical systems
differential_equations/
ordinary_differential_equations/
partial_differential_equations/
dynamical_systems/
ergodic_theory/
calculus_of_variations/
control_theory/
numerical_differential_equations/
fluid_dynamics_mathematics/
reaction_diffusion/
Probability and statistics
probability/
finite_probability/
random_variables/
distributions/
conditional_probability/
martingales/
stochastic_processes/
brownian_motion/
concentration_inequalities/
coupling/
random_matrices/
interacting_particle_systems/
stochastic_calculus/
probabilistic_method/
statistics/
estimation/
hypothesis_testing/
regression/
bayesian_statistics/
asymptotic_statistics/
nonparametric_statistics/
causal_inference/
information_theory/
statistical_learning_theory/
Geometry and topology
geometry/
euclidean_geometry/
affine_geometry/
projective_geometry/
convex_geometry/
discrete_geometry/
computational_geometry/
differential_geometry/
riemannian_geometry/
symplectic_geometry/
metric_geometry/
incidence_geometry/
geometric_group_theory/
topology/
point_set_topology/
algebraic_topology/
differential_topology/
geometric_topology/
low_dimensional_topology/
knot_theory/
homotopy_theory/
homology_and_cohomology/
manifolds/
topological_data_analysis/
Category theory and higher structures
category_theory/
basic_categories/
functors_and_natural_transformations/
limits_and_colimits/
adjunctions/
monoidal_categories/
enriched_categories/
higher_categories/
topos_theory/
categorical_algebra/
categorical_probability/
Discrete mathematics and theoretical computer science
discrete_mathematics/
finite_structures/
discrete_probability/
discrete_optimization/
recurrence_and_induction/
algorithms/
correctness/
termination/
complexity_bounds/
data_structures/
randomized_algorithms/
approximation_algorithms/
online_algorithms/
distributed_algorithms/
complexity_theory/
reductions/
np_completeness/
counting_complexity/
circuit_complexity/
communication_complexity/
parameterized_complexity/
proof_complexity/
formal_languages/
cryptography/
quantum_information/
quantum_computation/
Numerical and applied mathematics
numerical_analysis/
error_analysis/
interpolation/
numerical_integration/
numerical_linear_algebra/
verified_numerics/
interval_arithmetic/
applied_mathematics/
mathematical_physics/
continuum_mechanics/
elasticity/
thermodynamics/
electromagnetism/
relativity/
quantum_mathematics/
mathematical_biology/
epidemiology/
game_theory/
economics/
operations_research/
inverse_problems/
Mathematical methods and proof genres
These should be represented either as cross_domain/ packet families or controlled metadata tags because they recur across subjects.
proof_methods/
direct_proof/
contradiction/
contrapositive/
induction/
strong_induction/
minimal_counterexample/
infinite_descent/
extremal_principle/
invariants/
monovariants/
pigeonhole/
double_counting/
probabilistic_method/
compactness/
diagonalization/
generating_functions/
linear_algebra_method/
polynomial_method/
spectral_method/
entropy_method/
Fourier_method/
sieve_method/
discharging/
switching_arguments/
coupling/
compression/
certificate_replay/
Research artifact genres
research_genres/
theorem_formalization/
conjecture_audit/
verified_counterexample/
minimal_counterexample/
finite_classification/
computational_certificate/
formalization_wall/
missing_library_lemma/
corrected_statement/
conditional_theorem/
reduction_theorem/
asymptotic_bound/
algorithm_correctness/
complexity_proof/
benchmark_reconstruction/
independent_replication/
literature_reconciliation/
negative_result/
method_exhaustion/
reusable_abstraction/
Required packet-family ladder for every category
Every category should be filled using a common ladder rather than random theorem collection.
00_scope_and_vocabulary
01_definitions
02_canonical_examples
03_counterexamples_and_edge_cases
04_elementary_lemmas
05_proof_patterns
06_standard_exercises
07_core_theorems
08_equivalent_formulations
09_algorithms_and_certificates
10_failure_modes
11_cross_domain_bridges
12_advanced_theorems
13_research_surveys
14_recent_papers
15_open_problems
16_frontier_artifacts
17_missing_formal_infrastructure
18_verified_research_trajectories
19_publication_and_review
These numbers describe curriculum roles and may be encoded as metadata or manifests rather than physically nested directories if excessive nesting harms tooling.
Generic packet-campaign prompt
Add a reusable prompt t
8000
emplate such as agents/PACKET_CAMPAIGN_PROMPT.md or docs/packet-campaign-prompt.md.
You are building a verifier-gated MathCorpus packet family for:
CATEGORY: {{category}}
SUBCATEGORY: {{subcategory}}
TARGET LEVEL RANGE: {{level_start}} through {{level_end}}
FORMAL SYSTEM: Lean 4 with pinned Mathlib
PUBLICATION MODE: {{public_safe | quarantined | private_audit}}
Your job is to build a coherent machine curriculum from first principles to the current research frontier. Do not create a random list of theorem statements. Build a dependency-ordered concept graph whose packets teach, test, formalize, and extend the category.
TRUST BOUNDARY
1. A textbook, paper, website, model answer, or human explanation may supply candidate statements, definitions, proof ideas, citations, and provenance.
2. None of those sources proves a mathematical claim inside MathCorpus.
3. A formal theorem is `kernel_verified` only after the pinned Lean kernel accepts it through the tracked Proof Search workflow.
4. Failed attempts, rejected proofs, diagnostics, abandoned approaches, and missing declarations must be preserved as negative examples or repair trajectories.
5. Open-problem-adjacent work must state exactly what it does and does not prove.
6. Never infer novelty. Perform literature and contribution review before making a novelty claim.
PHASE A: MAP THE FIELD
- Define the scope and boundaries of the category.
- Build a vocabulary and notation map.
- Identify prerequisite categories and cross-domain dependencies.
- Collect authoritative pedagogy: introductory texts, advanced texts, lecture notes, surveys, reference works, and existing formal libraries.
- Collect research lineage: foundational papers, major theorems, standard methods, modern surveys, recent papers, active conjectures, and known counterexamples.
- Record every source in the hash-pinned literature catalog.
- Separate model-visible sources from post-hoc prior-art review.
PHASE B: BUILD THE CURRICULUM GRAPH
Create a dependency-ordered syllabus containing:
- definitions;
- canonical examples and nonexamples;
- minimal counterexamples;
- elementary lemmas;
- standard proof patterns;
- exercises at several difficulty levels;
- equivalent formulations;
- core theorems;
- algorithms and certificates where relevant;
- common misconceptions and failed proof routes;
- advanced theorems;
- research-level reductions;
- open problems and formalization walls.
For every proposed packet, specify:
- packet id and title;
- domain, level, kind, and difficulty;
- informal statement;
- proposed formal statement;
- prerequisite concepts and theorem dependencies;
- pedagogical role;
- proof method tags;
- source provenance;
- expected Mathlib coverage;
- verification plan;
- training eligibility and contamination risk;
- known ambiguity or fidelity risk.
PHASE C: INGEST PEDAGOGY
Use pedagogy to build concept packets, examples, exercises, and proof-pattern packets. Rewrite explanations in original language while preserving attribution and factual meaning. Do not copy protected text beyond permitted excerpts. Create multiple proof variants where useful:
- pedagogical;
- canonical;
- shortest;
- restricted tactic set;
- interactive step-by-step.
PHASE D: INGEST RESEARCH PAPERS
For each paper:
1. freeze bibliographic metadata and source version;
2. extract definitions, assumptions, theorem statements, lemmas, algorithms, experiments, and claimed dependencies;
3. perform statement-fidelity review;
4. reconstruct prior art and identify what is genuinely new in the paper;
5. divide the argument into formalization units;
6. classify each unit as already in Mathlib, straightforward bridge, major missing abstraction, computational certificate, analytic wall, or presently out of scope;
7. create packet candidates for all reusable units;
8. preserve all failed formalization routes;
9. seek author or domain-expert review before strong public claims.
PHASE E: FORMALIZE FROM FIRST PRINCIPLES
- Start from the lowest missing prerequisite, not from the paper's final theorem.
- Reuse existing Mathlib declarations after direct lookup.
- Do not declare infrastructure absent based on fuzzy search alone.
- Formalize reusable lemmas at the greatest faithful generality that remains reviewable.
- Promote cross-domain lemmas into shared packet families.
- Verify every formal result through a tracked episode.
- Preserve exact imports, toolchain, statement hash, proof hash, environment hash, diagnostics, and replay evidence.
PHASE F: ADVANCE TO THE FRONTIER
For frontier work, produce one or more of:
- a full kernel-verified theorem;
- a kernel-verified partial theorem;
- a verified reduction;
- a verified counterexample;
- an independently checked certificate;
- a precise formalization wall;
- a corrected or clarified statement;
- a reusable missing-library contribution;
- a provenance-complete negative result;
- a verified research trajectory.
Do not grade a campaign only by whether the headline theorem was solved. Grade it by verified frontier movement, reusable infrastructure, corrected knowledge, replayability, and the quality of the preserved trajectory.
PHASE G: VALIDATE AND PUBLISH
Before merging packets:
- validate against the packet schema;
- recompute canonical hashes;
- build and replay the Lean project;
- check dependency references and cycles;
- run redaction and contamination audits;
- deduplicate statements and proofs;
- verify source licenses and attribution;
- generate exact corpus statistics;
- create public-safe and audit exports separately;
- record independent review status;
- create a frozen release when a campaign reaches a stable checkpoint.
DELIVERABLES
Return:
1. a category map;
2. a dependency graph;
3. a prioritized packet backlog;
4. source and literature records;
5. packet JSON candidates;
6. paired Lean module plan;
7. negative-example plan;
8. research-paper formalization queue;
9. formalization-wall report;
10. validation and publication checklist.
Category-specific prompt overlays
The generic prompt should support small overlay files that add domain-specific requirements without duplicating the whole prompt.
Examples:
agents/overlays/graph_theory.md
agents/overlays/combinatorics.md
agents/overlays/analytic_number_theory.md
agents/overlays/probability.md
agents/overlays/algebraic_geometry.md
agents/overlays/verified_algorithms.md
A graph-theory overlay should require:
- graph model and finiteness assumptions;
- simple/multi/directed/weighted distinction;
- invariant definitions;
- isomorphism invariance;
- witness and counterexample encodings;
- independent certificate checker where appropriate;
- mutation tests for counterexample checkers;
- minimality claims separated from existence claims.
A combinatorics overlay should require:
- finite object encoding;
- counting convention;
- labeled versus unlabeled distinction;
- recurrence or generating-function normalization;
- bijection direction and inverse obligations;
- finite computation separated from universal proof;
- certificate format for enumerations and extremal claims.
An analytic-number-theory overlay should require:
- exact quantifier order and parameter dependencies;
- explicit constants versus asymptotic notation;
- real/complex measurability and integrability obligations;
- finite estimate layer separated from limiting theorem;
- imported analytic estimates treated as tracked assumptions until formalized.
Recommended initial implementation order
- Add a canonical category registry and aliases.
- Add curriculum-role metadata or manifests for the 00–19 ladder.
- Create the generic packet-campaign prompt.
- Add graph theory and combinatorics overlays first.
- Scaffold category directories with README scope files, not empty packet claims.
- Generate packet backlogs for graph theory, combinatorics, analytic number theory, probability, and optimization.
- Connect Proof Search MCIP export to automatic packet candidate generation.
- Add CI checks for valid category paths and category-registry references.
- Add dashboards showing packet counts, level coverage, missing prerequisites, and frontier walls by category.
Acceptance criteria
- A reviewed category registry covers the major mathematical subjects and research genres above.
- Category paths and aliases are machine-readable and schema-validated.
- Existing packets migrate without breaking canonical identity.
- Every category can represent packets from elementary definitions through frontier artifacts.
- The generic packet-campaign prompt is committed and references the actual schema/trust workflow.
- Domain overlays exist for at least graph theory, combinatorics, analytic number theory, probability, and verified algorithms.
- Category READMEs define scope, prerequisites, exclusions, canonical sources, and current formalization walls.
- A generated coverage dashboard reports levels, kinds, verification states, negative examples, and frontier gaps per category.
- Empty directories are not treated as corpus progress.
- Research-paper ingestion preserves source version, statement fidelity, prior art, contribution boundaries, and licensing.
- Formalization work enters only through tracked verifier-backed episodes.
- Proof Search MCIP imports can populate packet candidates and evidence without changing canonical proof authority.
- Public exports remain fail-closed for open problems, benchmarks, restricted proofs, and unclear licenses.
Non-goals
- Do not create one giant monolithic packet per field.
- Do not copy entire textbooks or papers into the corpus.
- Do not mark extracted theorem statements as verified.
- Do not equate directory coverage with mathematical coverage.
- Do not force all subjects into identical proof styles.
- Do not weaken the existing trust, provenance, redaction, or contamination controls.
Design note
The taxonomy will eventually outgrow any hand-written directory tree. Treat this issue as the first version of a controlled registry and curriculum graph, not a permanent claim that the hierarchy above is mathematically canonical. Packets should support cross-listing through metadata and dependency edges because many important areas belong to several domains at once.
Activity