Tutorials
Each tutorial starts with a concrete picture, then tightens into a precise model that tools can manipulate.
Tutorial 1: Approximate state tracking
Start inside a card counter’s head, then zoom out into state machines, abstraction, counterexamples, CEGIS, and the boundaries between heuristics and proofs.
Tutorial 2: Isomorphism
A 1-to-1, structure-preserving translation: why some “different abstractions” are the same thing in different clothes, and how to move problems into better toolchains.
Tutorial 3: Tau Language
Learn to read and write small executable specifications by listing invariants first, then letting a solver produce behaviors that satisfy them.
Tutorial 4: World models and continuous learning
Why internal models are more than prediction, why test-time learning is powerful, and why invariants and counterexamples become essential when the model can drift.
Tutorial 5: Reformulation and compression
How changing representations creates leverage, why abstraction rhymes with compression, and how neuro-symbolic gates turn model proposals into checkable evidence.
Tutorial 6: MPRD and the Algorithmic CEO
The neuro-symbolic gate from Tutorial 5 turned into production architecture. Models propose, rules decide, and counterexamples drive refinement.
Tutorial 7: What makes a good software engineer, and what clean code means
A user-centered framework for the agentic era: provenance-agnostic quality, diamond-rule engineering, and best-practice rails for safe, maintainable systems.
Tutorial 8: Predictive reading, scrambling, invariants, and proof
Build an interactive scrambler app, verify logic invariants, and separate formal proof from empirical proof-by-witness about human predictive reading.
Tutorial 9: Prompt engineering and precision communication
Reduce ambiguity by making structure explicit. Compare bad and good prompts, connect reformulation to state explosion, and try a small transpiler demo that turns controlled language into specs.
Tutorial 10: Reasoning, logic, and prediction
What reasoning is, why statistical learning cannot in principle produce logical validity, and why even approximate logic from a neural network cannot match a dedicated solver.
Tutorial 11: Attacking hard problems with Church's synthesis problem
Define Church synthesis precisely, trace what is decidable, then use a decomposition-plus-invariants workflow to run systematic, falsifiable attempts against the complexity wall.
Tutorial 12: Why current LLMs are not yet AGI
A scoped argument for the conceptual gap: strong language-pattern modeling is not yet the same as stable meaning creation, concept invention, or meaning-preserving formalization.
Tutorial 13: What reasoning is
Separate guessing, search, explanation, and proof using a child arithmetic example, Peano arithmetic, and the difference between discovery and justification.
Tutorial 14: Microkernels and micro-models
Use seL4 as a case study for shrinking the trusted core, proving small local contracts, and widening assurance through checked composition rather than monolithic proof blobs.
Tutorial 15: Exhaustive search and path integrals
Compare proof by exhaustive search with sum-over-histories, then extend the analogy to action, weighted futures, and the boundary between interference and intelligent planning.
Tutorial 16: Presburger arithmetic, the decidable island
Build Presburger arithmetic from zero and successor, read its formulas, understand why excluding multiplication makes every question decidable, and see how this fragment powers real verification tools.
Tutorial 17: Software shapes and ZenoDEX
Start from arcade, ATM, and vending-machine intuition, then compress those shared shapes into states and invariants before climbing into ZenoDEX, formal tools, and parameter synthesis.
Tutorial 18: ZenoDEX shape transition
Compare the old ZenoDEX shape with the achieved audited-domain Shape++, then track how exact formulas, proof-carrying boundaries, and chaos-engineering probes make disaster states unreachable.
Tutorial 19: Resolution, refutation, and falsification
Put logical refutation and Popperian falsification side by side, then separate proof in a closed formal world from corroboration in an open empirical world using explicit formulas.
Tutorial 20: Neuro-symbolic reasoning and witness spaces
Treat LLMs as existential engines and symbolic methods as universal verifiers, then map proof search, counterexample search, synthesis, experiment design, and coverage limits in one formula family.
Tutorial 21: A perceptron in Tau Language
Build a perceptron from formulas, execute bounded classifier specs in Tau, inspect real traces, and then separate the replayable classifier lane from a host-side learning loop.
Tutorial 22: Medical deciders, MPRD, and Tau
Map bounded medical workflows into the MPRD shape, then use educational Tau policies to separate model proposals from execution authority through fail-closed guideline gates and human escalation paths.
Tutorial 23: Decidable medical machines, from formulas to Tau
Start with a calorie calculator and a kidney follow-up workflow, then view each one as math, logic, a decision tree, a finite-state machine, ordinary code, and a downloadable Tau spec.
Tutorial 24: Consciousness, computationalism, and Rice's theorem
Make one controversial argument precise: if consciousness is a nontrivial semantic property of computation, then no general Turing-machine detector can decide it from arbitrary encodings of programs.
Tutorial 25: Quantifier factoring and neuro-symbolic loop engineering
Start from "LLM = existential engine, formal tool = universal verifier", then push downward into counterexample search, certificate compression, quantified games, quotients, and fixed-point reasoning.
Tutorial 26: Galois loops and obligation carving
Reframe CEGIS through a Galois and FCA lens, prove the bounded obligation-side policy-improvement loop, show its measured power on finite relation universes, and sharpen the next frontier into controller compression.
Tutorial 27: Verifier-compiler loops
Start from plain CEGIS, then ask when verifier behavior itself can be compressed into a reusable symbolic controller for routing, ranking, and fail-closed pre-screening without replacing the exact gate.
Tutorial 28: Profit agents, post-AGI economics, and mechanism design
Study bounded toy economies for profit agents under explicit assumptions, then climb from platform incentives and demand closure to routing, trust, assurance, and mechanism design.
Tutorial 29: Loop-space geometry
Factor neuro-symbolic loops into witness languages, quotients, separator policies, label bases, and compiled artifacts, then study why some loops are structurally stronger than others.
Tutorial 30: Counterexample-guided requirements discovery
Recover missing requirements from witness structure, observation quotients, and minimal separator policies instead of treating stakeholder follow-up as one undifferentiated escape hatch.
Tutorial 31: Hybrid geometry-changing loops
Compare direct control with loops that reshape ambiguity geometry first, then compile or control only the residue that remains.
Tutorial 32: Temporal label functions and staged bases
A focused lesson on temporal label functions: why a richer basis can be strictly finer on the whole family, yet become exact only after the right first carve.
Tutorial 33: Formal neural networks
What would it take for a neural network to count as a computer in a strong sense, and what routes could get there?