Course Catalog & Credential Pathway — Dwg. No. PF-002E
A field branch of the Construction Track, for students aimed at formal mathematics and machine-assisted discovery — search and verification pointed at open problems instead of open-ended chat.
Field branch of Dwg. No. PF-002, The Construction Track — same core sequence through Phase II, concentrated here into formal proof & automated search from Phase II onward. See also Dwg. No. PF-001, The Verification Track.
Five core strands, plus the domain strand this branch concentrates in
No frameworks yet, and no formal logic yet either. Two years of straight math and programming fundamentals, identical to the core Construction Track.
Precalculus, Accelerated
Compressed to clear room for calculus by grade 11 — the standard on-ramp for anyone headed toward a quantitative degree.
Programming I — Python
Variables, control flow, functions, data structures. Fluency, not tricks.
Discrete Mathematics & Logic
Sets, proofs, graphs, combinatorics — the math CS theory actually runs on, usually skipped until it's overdue.
Technical Writing for Research
Writing a clear methods section and an honest results section — the two paragraphs every paper lives or dies on.
The math and CS sequences converge into an actual first model, same as the core track. The formal-proof layer begins concurrently — by the end of Phase II a student can both train a small model and write a fully formalized proof in a real theorem prover.
Calculus I & II
Through multivariable and the gradient — backpropagation is the chain rule with bookkeeping, and it should read that way.
MATH 101
Linear Algebra
Vector spaces, eigendecomposition, matrix calculus. Every tensor operation is this course wearing a framework's syntax.
MATH 101
Probability & Statistics for ML
Distributions, estimation, Bayes — framed toward loss functions and uncertainty, not toward the social-science stats track.
Data Structures & Algorithms
Complexity analysis and the standard structures, drilled to fluency — still the baseline technical-interview bar at every AI lab.
CS 100
Intro to Machine Learning
Regression through a first neural net, built from array operations before any framework is allowed to hide the mechanics.
MATH 210, STAT 220
Research Seminar — Reading Group
Weekly seminal-paper reads (perceptron through transformers), presented and defended aloud, not just summarized.
Formal Logic & Proof Structure
Propositional and predicate logic, proof strategy, and the discipline of a fully formal argument — what separates a proof from a convincing sketch of one.
MATH 210
Interactive Theorem Proving
Lean and Coq in practice — formalizing existing proofs, then extending them, in the same proof assistants now used to verify machine-generated results.
MATH 225, CS 210
Here the domain degree takes over from the general CS/applied-math track. A pure mathematics-plus-CS program replaces DEG 300 — the depth of mathematical training, not the tooling, is what makes a formalized-proof result trustworthy.
Pure Mathematics Degree
Formal core in a pure mathematics-plus-CS program — the mathematical depth that makes a search-and-verify result trustworthy, not just plausible.
Search & Evolutionary Program Synthesis
Evolutionary and LLM-guided search over formal search spaces — the AlphaEvolve pattern — applied to an open problem in algorithms, combinatorics, or number theory the student picks and pursues.
PRF 235, ML 230
Deep Learning for Search & Discovery
Large-scale search, program synthesis, and the LLM-guided-evolution methods behind systems like AlphaEvolve, taught directly against an open mathematical problem rather than as a generic survey.
ML 230
Systems for ML
Distributed training, GPU/accelerator programming, and the infrastructure a large-scale automated-search run needs to explore a search space at any real breadth.
CS 210
Supervised Research Practicum
Placement inside a formal-methods or mathematical-discovery research group, with a mentor of record. Graded on a reproduction that actually reproduces, or a contribution that gets merged.
RES 240, ML 310
Capstone — Build & Ship
One model or tool — a formalized proof of an open lemma, a search-and-verify pipeline against a real conjecture list — taken from idea to a deployed, load-bearing artifact with real users.
ENG 320, RES 350
No end date: the ML baseline moves every conference cycle, and the open-problem baseline — the Erdős problems and their kin — moves on its own slower schedule that a purely computational graduate can lose track of.