The Future of Math Education: Proofs You Can Run (Part 3 of 3)

We've covered the philosophy (Part 1) and the geometry (Part 2). Now let's talk about why simplicial homotopy type theory isn't just beautiful mathematics—it's a practical tool that could transform education. The secret? Proofs that compute.

The Curry-Howard Correspondence: Proofs = Programs

There's a deep connection in computer science called the Curry-Howard correspondence:

In sHoTT, this connection is fundamental. When you prove something, you're literally writing a program. When you verify a proof, you're running a type-checker.

// In a proof assistant like Agda or Lean, proofs ARE code

// This TYPE represents the proposition "A implies B"
type Implies<A, B> = (proof: A) => B;

// This FUNCTION is a proof that implication is transitive
function transitivity<A, B, C>(
  proofAB: Implies<A, B>,
  proofBC: Implies<B, C>
): Implies<A, C> {
  return (proofA: A) => proofBC(proofAB(proofA));
}

// The code compiles = the proof is valid!

Proof Assistants: Your Math IDE

Just like programmers have IDEs that catch errors, mathematicians now have proof assistants that verify their work:

• Lean: Used to formalize thousands of theorems (see mathlib)
• Agda: Beautiful syntax, perfect for homotopy type theory
• Coq: Battle-tested, used for critical software verification

These tools give you:

1. 1Immediate feedback — errors are caught as you type
2. 2Autocomplete for proofs — the system suggests next steps
3. 3Guaranteed correctness — if it compiles, it's mathematically valid

"Imagine if every math homework assignment came with a 'Run' button that told you instantly whether your proof was correct."

Why sHoTT Makes This Even Better

Standard type theory already has the proof-as-program connection. sHoTT adds the geometric layer:

• Paths ARE data — equivalence proofs carry computational content
• Higher structure is explicit — no hidden assumptions
• Univalence axiom — equivalent things can be substituted freely

// In sHoTT, these two types are not just "isomorphic"—
// they're EQUAL in a way you can compute with

// Type A: Integers as {..., -2, -1, 0, 1, 2, ...}
// Type B: Pairs (sign, magnitude) like ('+', 5) or ('-', 3)

// The univalence axiom says: since we can convert perfectly
// between A and B, they ARE the same type.
// Any theorem proved about A automatically applies to B!

The Educational Revolution

Emily Riehl and other mathematicians are pushing to make sHoTT the starting point for math education—not an advanced topic you reach after years of prerequisites.

Why this could work:

1. 1Aligns with computation — students already think in algorithms
2. 2Visual by design — shapes and paths, not abstract axioms
3. 3Matches modern practice — this is how research mathematics actually works
4. 4Immediate verification — proof assistants provide instant feedback

The analogies are everywhere:

Getting Started

Want to explore these ideas yourself? Here's a path:

1. 1Play with Lean — try the Natural Number Game
2. 2Watch Emily Riehl's lectures — search "infinity categories for undergraduates"
3. 3Read "Homotopy Type Theory: Univalent Foundations" — free online (challenging but rewarding)
4. 4Build things — implement simplicial complexes in your favorite language

// A simple simplicial set you can play with
class SimplicialSet {
  constructor() {
    this.simplices = new Map(); // dimension -> list of simplices
  }
  
  addSimplex(dimension, vertices) {
    if (!this.simplices.has(dimension)) {
      this.simplices.set(dimension, []);
    }
    this.simplices.get(dimension).push(vertices);
  }
  
  // Check if we have all faces of a simplex
  hasAllFaces(vertices) {
    // Every subset should exist in the lower dimension
    // This is the "closure" property of simplicial sets
    return vertices.every((_, i) => {
      const face = vertices.filter((_, j) => j !== i);
      return this.simplices.get(face.length - 1)?.some(
        s => s.every((v, k) => v === face[k])
      );
    });
  }
}

The Bottom Line

Mathematics education is ripe for disruption. The set-theoretic foundations we currently teach are:

• Historically contingent, not pedagogically optimal
• Disconnected from computation and geometry
• A barrier to accessing modern mathematics

sHoTT offers a path forward: rigorous yet intuitive, abstract yet computational, foundational yet accessible.

The question isn't whether this shift will happen—it's whether you'll be part of making it happen.

Thanks for joining this 3-part journey through simplicial homotopy type theory. The future of mathematics is geometric, computational, and waiting for curious minds like yours to explore it.