Evidence

Claim-level traceability, with boundaries visible.

Last reviewed: July 4, 2026 · Lean mapping 2026-05-07

TheoremPath records exact mappings from governed claims to checked Lean theorem artifacts. The current formal layer covers selected probability, statistics, and learning-theory results, with broader public claims kept in source review until their Lean wrappers are present.

This page also separates product contracts from research evidence: a signed-in smoke can prove that state is written and read, but it does not prove learning lift, calibrated item difficulty, or an IRT model fit.

Product truth contract

The adaptive layer is instrumented, not validated as an outcome claim.

The implemented learner loop can save state, connect attempts to the graph, and schedule reviews. The evidence bar is higher for claims about improved learning, calibrated ability, or item discrimination. Those claims require enough real signed-in data and comparison against baselines.

FSRS

scheduler signal

FSRS-style review state estimates card retrievability from review timing and grades. It can decide what is due for review; it is not a proof of mastery or a claim that the learner understands the theorem.

Q-matrix

coverage map

The Q-matrix links questions to skills, claims, and prerequisites. It explains what an item is meant to test; it is not a causal proof that a missed item has one unique cause.

PFA

guarded fit lane

Performance Factor Analysis is the planned interpretable fit over practice opportunities and correctness. Current production rows are data-insufficient, so PFA stays behind calibration gates instead of being presented as a validated personalization model.

Lean-checked entries

TheoremPath declarations that compile in CI with zero recorded sorry/admit markers.

Formalized claims

Checked formal statements whose recorded scope matches the governed claim.

Dependency formalized

Checked supporting lemmas that do not by themselves prove the full public claim.

sorry / admit

Lean placeholders across these checked entries: sorry=0, admit=0.

Operating dashboard

Gaps are part of the evidence record.

These counts are generated from governed claims, source-location records, the Lean manifest, assessment links, and published topic MDX. The point is not a trust badge; it is a work queue with visible missing pieces.

Governed claims

1,223

Claim records tracked in the public governance index.

Flagship trail coverage

12/12

0 missing trail requirements across theorem-first paths, including the two failure-check floor.

Atlas traces

48 curated checkpoints; 0 missing trace requirements.

Source locators

153/153

100% of source-supported claims resolve to source-location IDs.

Lean mapping

118 source-supported formal claims still need manifest entries; 3 are explicit source-only deferrals.

Source-only formal

Broad source-reviewed theorem claims that are deliberately not treated as Lean-mapping tasks yet.

Diagnostic items

160

152/153 source-checked claims have canonical item links.

Missing theorem blocks

613/659 published topics include theorem blocks.

Missing exercise blocks

619/659 published topics include exercise blocks.

Structure queue

Published topics missing theorem or exercise blocks across 659 topics.

Research quality queue

Ranked from the generated coverage report. Each row points to the first concrete gap to close in that work lane.

4 active lanes

01
Collect diagnostic calibration data
Real usage is below the publication threshold. Item difficulty: 6/30.
#evidence-calibration-difficulty
0/6
usage milestones met
02
Map source-checked theorems to Lean
Source-supported formal claims should either have a Lean manifest entry or remain visibly source-only.
/topics/inner-product-spaces-and-orthogonality#claim-evidence
118/153
formal claims without Lean
03
Add canonical diagnostics to checked claims
Claims with evidence should have at least one diagnostic item that tests the exact assumption or theorem.
/topics/bayesian-optimization-for-hyperparameters#claim-evidence
1/153
checked claims without diagnostics
04
Close theorem and exercise structure gaps
Published topics without theorem or exercise blocks should be fixed or kept out of flagship paths.
/topics/agent-based-modeling-with-ml#topic-mdx-content
46/659
published topics with structure gaps

Source locator gaps

All source-supported claims currently resolve to source-location IDs.

Lean mapping gaps

118

Source-only formal claims

Diagnostic gaps

GP-UCB Cumulative Regret BoundSource-checked claim has no canonical diagnostic link.bayesian-optimization-for-hyperparameters

Topic structure gaps

Flagship trail audit

Every flagship theorem trail currently satisfies the theorem-first contract, including at least two evidence-linked failure checks.

Atlas trace checkpoints

Every curated theorem trace currently exposes edge reasons, checkpoints, and trail links.

Audit receipts

Learner loop contracts: 15/15 All checks covered.

Required smoke gates before calling this production-ready: route shell, signed-in web state, account deletion guard, iOS continuity, Browser and iPhone proof assets, and Signed-in iPhone visual walkthrough receipts.

Covered means the contract exists and has a receipt. It does not mean the study policy is empirically better than a baseline or that the psychometric model is calibrated.

Source receipt: data/content/learner-loop-readiness.json. Generated July 14, 2026.

Q-matrix rows: Diagnostic items are tied back to the same governed claim and skill graph.
Claim links: Claim-to-assessment links are treated as reviewable evidence, not page decoration.
Content gaps blocking trails: Open trail blockers stay visible until the flagship audit is clean.
Failure modes: Trail checks must include at least two evidence-linked failure checks before promotion.

Open production health Open sign-up flow Open iOS graph contract Open gap finder

Open route

Markov tail bound Chebyshev variance tail Finite union bound Hoeffding lemma Hoeffding finite-sum bound Finite-class uniform convergence

Inspect learner-loop receipt rows

Public route shell (covered)
Home, Atlas, Evidence, sign-up, learner home, and Profile routes exist in the current branch.
Signed-in web launch gate (covered)
The required signed-in smoke has a preflight that rejects localhost, stale host state, missing smoke email, unsafe deletion aliases, and stale public learner-loop contracts. A fresh-user wrapper chains the public contract, the iOS companion source contract, the iOS intended API contract, Clerk test-auth onboarding storage-state capture for +clerk_test accounts, intended walkthrough, a post-walkthrough bearer-token refresh, and required-by-default iOS signed-in continuity with a non-logged bearer-token file handoff. If destructive deletion is enabled with iOS continuity, deletion runs last so iOS can read the account state before removal.
Diagnostic persistence (covered)
Signed-in diagnostic submissions write diagnostic attempts, learning events, event logs, and evidence envelopes.
Saved, review, and Profile state (covered)
The intended signed-in walkthrough answers a saved diagnostic item, then exercises a saved topic, review entry point, learner home evidence, Profile identity, and authenticated API receipts for saved, diagnostic, review, and mastery state.
Account deletion guard (covered)
Deletion smoke is gated behind an explicit flag and a disposable +tp-delete- alias, then verifies the deleted account no longer has a live API profile.
No PII in learner-loop events (covered)
Product-loop events redact sensitive keys and values; typed learning events reject raw learner text metadata.
Evidence dashboard inputs (covered)
Claims=1223, Lean mappings=56, source locators=135, diagnostic items=3443, Q-matrix rows=14426, claim links=177, content gaps=10.
Flagship theorem trails (covered)
Flagship audit reports 12/12 trails under the machine contract.
Atlas trace checkpoints (covered)
Atlas path responses include traversal-order reasons/checkpoints, the UI renders them, and check:atlas-paths enforces the contract.
iOS companion contract (covered)
The tracked iOS contract receipt covers the companion contract, intended public API probe, bearer-token continuity probe, TestFlight readiness check, simulator tests, and simulator build-run.
Latest public deployment contract smoke (covered)
Latest verified public learner-loop smoke passed against https://theorempath.com with THEOREMPATH_EXPECTED_GIT_SHA=f08ec233488add2af375eb15c36b6fbe3c197b6a. The current live production SHA is reported separately by /api/health so this static receipt does not pretend to prove its own future deploy commit.
Fresh signed-in production/staging smoke (covered)
Fresh disposable-account smoke passed against production: public contract, Clerk test-auth onboarding without OTP, diagnostic completion, beta topic save, daily review, learner home, Profile identity, post-walkthrough bearer-token refresh, persisted API receipts, and deletion-only account removal after iOS continuity. Raw smoke email and bearer token were not stored.
iOS signed-in API continuity (covered)
iOS signed-in API continuity passed against production using the refreshed non-logged bearer-token file from the fresh web smoke: /api/v1/me, saved beta-distribution state, diagnostic attempts, review today, and mastery state were readable for the same disposable account before deletion.
Browser and iPhone proof assets (covered)
The proof receipt tracks one production browser evidence-dashboard capture plus iOS simulator Today, Atlas, Saved, and Profile screenshots under data/content/learner-loop-demo-capture.json.
Signed-in iPhone visual walkthrough (covered)
Signed-in fresh-install iOS screenshots show the same disposable production smoke account in Today, Saved, Atlas, and redacted Profile; the API continuity probe also passed for that account.

Usage calibration

Diagnostics are calibrated only where real usage supports it.

This block is generated by npm run psychometrics:report from LearningEvent rows. It separates item difficulty, item skip rate, item discrimination, review conversion, and later performance after review.

Implemented today

Signed-in learner state, Q-matrix links, review events, saved topics, profile identity, and iOS API continuity have contract receipts.

Not claimed yet

The saved report is still data-insufficient for item calibration or IRT. No public claim should treat the current samples as a fitted psychometric model.

Next evidence

Collect enough real signed-in attempts per item, then compare review and recommendation policies against baselines before promoting effectiveness claims.

Open psychometrics audit20 AssessmentAttempt rows · 146 LearningEvent rows · 11 DiagnosticAttempt runs

snapshot June 28, 2026

Calibration state

Sparse

Real usage rows exist, but sample sizes remain below calibration thresholds.

Answer events

142

Non-review LearningEvent rows used for item difficulty and discrimination.

Difficulty usable

Items with enough observations for empirical difficulty estimates.

Skip rate

Items with recorded skipped answers in the current usage report.

Discrimination usable

Items with enough learner contrast for high-minus-low ability separation.

Review conversion

0/12

Weak diagnostic answers that were followed by a review event.

Review effect pairs

Weak diagnostic answers followed by review and a later performance event.

Unreviewed pairs

Weak diagnostic answers without review but with later performance, used as a comparison group.

Readiness milestones

Best observed item-level counts against the publication thresholds. Source: database · 146 LearningEvent rows.

0/6 met

Item difficulty

6/30

24 more needed on one item.

Skip rate

6/30

24 more needed on one item.

Item discrimination

2/30

28 more needed on one item.

Review conversion

2/10

8 more needed on one item.

Later performance after review

0/10

10 more needed on one item.

Unreviewed comparison

0/10

10 more needed on one item.

Next collection targets

Item-level targets from the same saved usage report. These are collection instructions, not calibration claims.

6 open

Item difficulty
question:diverse-spot-error-002
24 more events with scored answer outcomes.
6/30
Open topic Collect signal
Skip rate
question:diverse-spot-error-002
24 more events with answer or skip outcomes.
6/30
Open topic Collect signal
Item discrimination
question:diverse-spot-error-002
28 more events from learners with other answered items.
2/30
Open topic Collect signal
Review conversion
question:diverse-counterexample-002
8 more events where weak diagnostic answers enter review.
2/10
Open topic Collect signal
Later performance after review
question:activation-relu-dead-neurons-004
10 more events where reviewed weak answers get later performance.
0/10
Open topic Collect signal
Unreviewed comparison
question:activation-relu-dead-neurons-004
10 more events where unreviewed weak answers get later performance.
0/10
Open topic Collect signal

Item difficulty: 6/30.
Skip rate: 6/30.
Item discrimination: 2/30.
Review conversion: 2/10.
Later performance after review: 0/10.

Calibration policy

difficulty n: 30
discrimination learners: 30
review opportunities: 10
effect pairs: 10
later window: 30d
simulation: excluded

Difficulty collection queue

question:linear-algebra-path-012
inner-product-spaces-and-orthogonality · n=2
Open topic Run diagnostic
n=2/30
question:linear-algebra-psd-pd-009
positive-semidefinite-matrices · n=2
Open topic Run diagnostic
n=2/30
question:inner-product-gram-schmidt-020
inner-product-spaces-and-orthogonality · n=1
Open topic Run diagnostic
n=1/30
question:inner-product-orthogonal-complement-021
inner-product-spaces-and-orthogonality · n=1
Open topic Run diagnostic
n=1/30

Skip-rate collection queue

question:linear-algebra-path-012
inner-product-spaces-and-orthogonality · n=2
Open topic Run diagnostic
n=2/30 · skip observed 100%
question:linear-algebra-psd-pd-009
positive-semidefinite-matrices · n=2
Open topic Run diagnostic
n=2/30 · skip observed 100%
question:inner-product-gram-schmidt-020
inner-product-spaces-and-orthogonality · n=1
Open topic Run diagnostic
n=1/30 · skip observed 100%
question:inner-product-orthogonal-complement-021
inner-product-spaces-and-orthogonality · n=1
Open topic Run diagnostic
n=1/30 · skip observed 100%

Discrimination queue

No item has enough learner contrast for discrimination yet.

Review conversion queue

question:diverse-counterexample-002
maximum-likelihood-estimation · n=2
Open topic Run diagnostic
0/2 reviewed
question:activation-relu-dead-neurons-004
activation-functions · n=1
Open topic Run diagnostic
0/1 reviewed
question:ei-spot-error-009
stochastic-gradient-descent-convergence · n=1
Open topic Run diagnostic
0/1 reviewed
question:la-drill-rank-nullity-021
vectors-matrices-and-linear-maps · n=1
Open topic Run diagnostic
0/1 reviewed

Later performance queue

No reviewed item has enough later-performance pairs yet.

Status labels

Formalized: The checked Lean theorem matches the governed claim scope.
Dependency formalized: A supporting lemma is checked, and the broader public claim is waiting on additional assumptions or proof steps.
Source-reviewed outside Lean: The claim can be source-supported while carrying no Lean proof badge on this page.

One complete trace: Markov's inequality

A serious evidence record should be inspectable. This example shows the informal claim, the formal theorem, and the boundary of that mapping.

Claim ID	claim:concentration-inequalities::markov-inequality
Informal claim	For a nonnegative random variable, tail probability is bounded by expectation divided by the threshold.
Formalized as	real-valued integrable Markov inequality with explicit nonnegativity, integrability, and positive-threshold assumptions
Lean declaration	TheoremPath.Probability.Concentration.markovInequalityRealIntegrable
Boundary	This Lean wrapper verifies the recorded real-valued Markov statement; broader concentration variants have separate claim records.

Lean theorem statement

theorem markovInequalityRealIntegrable
    {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} {X : Ω → ℝ} {t : ℝ}
    (hNonneg : 0 ≤ᵐ[μ] X) (hIntegrable : Integrable X μ) (ht : 0 < t) :
    μ.real {ω | t ≤ X ω} ≤ (∫ ω, X ω ∂μ) / t

Reproducibility: from verification/lean, run lake build. The public counts are derived from the checked Lean mapping and require zero recorded sorry or admit.

Verification boundary

Many governed claims are source-reviewed or draft-reviewed while waiting for a linked Lean theorem.
The finite-class uniform convergence entry is still a dependency formalization; the full stochastic theorem is tracked as a later composition target.
Active learning-theory proof lanes include iid sampling, bounded-loss instantiation, measurability of hypothesis classes, and closed-form sqrt/log rearrangements.
Lean proof evidence sits alongside source review for empirical, historical, implementation, and frontier-model claims.

Examples from the Lean mapping

Each card records the checked declaration, the theorem scope, and whether it formalizes the governed claim or only a dependency.

concentration inequalities

Markov Inequality

Formalized

In plain English

A nonnegative random variable with small expectation cannot be large very often.

Role in the graph

This is the first tail-bound bridge from averages to probability guarantees.

Checked theorem

TheoremPath.Probability.Concentration.markovInequalityRealIntegrable

Claim scope

real integrable nonnegative markov inequality

Proof scope

exact mathlib wrapper for markov

Mathlib theorem

MeasureTheory.mul_meas_ge_le_integral_of_nonneg

Exact claim-facing mathlib wrapper for Markov's inequality in real-valued integrable form. The finite weighted-support theorem remains a bridge proof, not the canonical verification target.

Checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c

concentration inequalities

Hoeffding One Sided Finite Sum

Formalized

In plain English

A bounded finite sum has an exponential one-sided deviation bound under the recorded assumptions.

Role in the graph

This is the concentration step behind finite-class generalization arguments.

Checked theorem

TheoremPath.Probability.Concentration.hoeffdingBoundedFiniteSumTail

Claim scope

finite centered sum bounded hoeffding one sided

Proof scope

exact mathlib wrapper for bounded hoeffding finite sum tail

Mathlib theorem

ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc, ProbabilityTheory.iIndepFun.comp, ProbabilityTheory.HasSubgaussianMGF.measure_sum_ge_le_of_iIndepFun

Exact claim-facing wrapper for the one-sided finite-sum Hoeffding bound for bounded independent real random variables.

Checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c

subgaussian random variables

Hoeffding Lemma

Formalized

In plain English

A bounded centered random variable has a sub-Gaussian moment-generating-function bound.

Role in the graph

This is the standard bridge from bounded variables to Hoeffding-style tails.

Checked theorem

TheoremPath.Probability.Concentration.hoeffdingLemmaBoundedCenteredSubgaussianMGF

Claim scope

bounded centered real subgaussian mgf

Proof scope

exact mathlib wrapper for hoeffding lemma

Mathlib theorem

ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero

Exact mathlib wrapper for Hoeffding's lemma in sub-Gaussian MGF form. Source review now permits claim-level display without implying the whole page is Lean verified.

Checked April 29, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c

measure theoretic probability

Borel Cantelli First

Formalized

In plain English

If event probabilities are summable, the limsup event has probability zero in the mathlib formulation.

Role in the graph

This turns a previous finite bridge into a direct probability theorem wrapper.

Checked theorem

TheoremPath.Probability.BorelCantelli.borelCantelliFirstLimsupMeasureZero

Claim scope

first borel cantelli limsup atTop ennreal

Proof scope

exact mathlib wrapper for first borel cantelli

Mathlib theorem

MeasureTheory.measure_limsup_atTop_eq_zero, MeasureTheory.ae_eventually_notMem

Exact claim-facing mathlib wrapper for the first Borel-Cantelli lemma in limsup-measure-zero form. The finite union-bound artifacts remain supporting bridge proofs, not the source of verification.

Checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c

kolmogorov probability axioms

Probability Measure Finite Union Bound

Formalized

In plain English

The probability of a finite union is at most the sum of the individual probabilities.

Role in the graph

This is a foundational tool used throughout concentration and learning theory.

Checked theorem

TheoremPath.Probability.KolmogorovAxioms.probabilityMeasureFiniteUnionBound

Claim scope

probability measure finite union bound

Proof scope

exact mathlib wrapper for probability measure finite union bound

Mathlib theorem

MeasureTheory.measure_biUnion_finset_le

Exact claim-facing wrapper for the finite union bound for probability measures.

Checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c

common inequalities

Cauchy Schwarz Inequality

Formalized

In plain English

The absolute inner product is bounded by the product of the two norms.

Role in the graph

This is a reusable inequality across linear algebra, statistics, and optimization.

Checked theorem

TheoremPath.LinearAlgebra.CommonInequalities.cauchySchwarzRealInner

Claim scope

real inner product space cauchy schwarz

Proof scope

exact mathlib wrapper for cauchy schwarz core

Mathlib theorem

abs_real_inner_le_norm

Exact claim-facing mathlib wrapper for the core Cauchy-Schwarz inequality in real inner product spaces. Equality, probability, and finite-sum variants remain separate explanatory scopes until governed separately.

Checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c

vc dimension

Sauer Shelah Lemma

Formalized

In plain English

A finite set family with bounded VC dimension cannot shatter too many subsets.

Role in the graph

This is a core combinatorial bridge behind classical learning-theory capacity bounds.

Checked theorem

TheoremPath.LearningTheory.VCDimension.sauerShelahFiniteSetFamily

Claim scope

finite set family sauer shelah binomial sum

Proof scope

exact mathlib wrapper for sauer shelah binomial sum

Mathlib theorem

Finset.card_le_card_shatterer, Finset.card_shatterer_le_sum_vcDim

Exact claim-facing mathlib wrapper for the finite set-family Sauer-Shelah binomial-sum bound. The common (em/d)^d analytic estimate is treated as a downstream corollary, not as part of this verified claim.

Checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c

uniform convergence

Finite Class Uniform Convergence

Dependency formalized

In plain English

The checked artifact is a scoped reduction step toward the finite-class uniform convergence theorem.

Role in the graph

It is useful evidence, but it is deliberately not labeled as the full stochastic theorem.

Checked theorem

TheoremPath.LearningTheory.UniformConvergence.finiteClassEpsilonRepresentativeHighProbabilityFromOneSidedTails

Claim scope

finite class epsilon representative failure probability from one sided risk deviation tails

Proof scope

scoped high probability risk bridge for finite class uniform convergence

Mathlib theorem

MeasureTheory.measure_union_le, TheoremPath.Probability.FiniteUnionBound.finiteMeasureUnionBound, MeasureTheory.ofReal_measureReal, ENNReal.ofReal_le_ofReal

Scoped bridge artifact for finite-class uniform convergence. It proves the risk-facing high-probability reduction from paired one-sided true-risk/empirical-risk deviation tail bounds and a delta-sized finite-class union-bound expression to a simultaneous epsilon-representative failure bound, and now includes fixed-hypothesis empirical-average upper- and lower-tail Hoeffding bridges with explicit sample-size hypotheses plus ENNReal adapters for the measure-valued union-bound layer; it does not verify iid sampling as the data-generating model or the closed-form sqrt/log sample-complexity display.

Checked April 30, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c

Diagnostic assumption links

A diagnostic item can be mapped to the exact assumption or theorem it tests. The Hoeffding slice records separate links for independence, the boundedness-to-sub-Gaussian step, and the finite-class union-bound step.

These mappings are evidence for learner state. They are not public theorem badges, and they should be audited like any other claim-to-source or claim-to-Lean link.

What waits before public badges

Evidence panels must show claim scope, not just page-level status.
Dependency formalizations must be visually distinct from exact claim wrappers.
Topic pages need stable source and diagnostic links before any trust indicator is promoted.

For the rules behind this page, see methodology. For all 56 verified theorems, see the Lean verification dashboard. For the theorem list, see key theorems.