Tutorials

Hands-on track: interactive labs

Prefer the bounded demos first? The labs page collects the interactive companions for witness search, loop geometry, verifier compilation, and state-machine exploration in one place.

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?

Tutorial 34: Neuro-symbolic DeFi defense

Use the USD 285M Drift Protocol exploit as a case study for compositional disaster-state analysis, then build the neuro-symbolic defense loop that catches multi-vector attacks before deployment and at runtime.

Tutorial 35: Concolic testing and branch exploration

Learn branch exploration as witness search: concrete execution gives one real path, symbolic path constraints steer the next run, and the modern practical story is hybrid.

Tutorial 36: Grammar-based fuzzing and structured search

Learn structured witness search over grammars, see why syntax preservation reallocates budget into semantic execution, and understand where concolic escalation and neural proposal do and do not belong.

Tutorial 37: The countable Cantor algebra and its completion

Learn why the clopen algebra of Cantor space is the unique countable atomless Boolean algebra, what its completion adds, and why classical completion is not yet an executable runtime story.

Tutorial 38: TABA, formula by formula

Learn the Boolean-algebra machinery behind TABA, read the quantifier-elimination and guarded-successor formulas step by step, and see which future extensions are plausible from the current literature.

Tutorial 39: Safe infinite-recursive tables in Tau Language

Study the safe table fragment for Tau, including pointwise revision, fixed-point semantics, runnable demos, and the boundary between this prototype and full TABA tables.

Tutorial 40: Optimizing Tau Language, Part I

Learn why Tau qelim optimization is a fragment-dispatch problem, read the compiled-forgetting formulas exactly, and see how guarded BDD and CNF-native routes can speed up scoped formulas.

Tutorial 41: Temporal Tau, Part I

Learn how bounded LTL-style operators fit Tau, why finite-horizon temporal formulas are decidable on finite carriers, and how this creates a new optimizer layer.

Tutorial 42: Optimizing Tau Language, Part II

Learn how certificate-carrying optimizers let Tau search for aggressive rewrites while accepting only the candidates whose certificates pass a trusted checker.

Tutorial 43: Optimizing Tau Language, Part III

Learn how a feature-flagged Tau diagnostic detects blowup risk before solving, why unused-variable compression is the first exponent to measure, and how route prediction can help without replacing proof certificates.

Tutorial 44: Official LTL(ABA) in Tau Language

Learn Ohad Asor's upstream Tau LTL(ABA) design, compare it to the bounded Temporal Tau fragment, and see why qlt, dyadic, and nlang matter.

Tutorial 45: Controlled English and explanation certificates

Turn one readable governance sentence into a checked two-variable counting formula, then prove that local failure certificates explain exactly when the rule fails.

Tutorial 46: Bounded game tables in Tau Language

Build a proof-backed finite game-table experiment for Tau, then use profitable-deviation evidence to prune strategically impossible profiles.

Tutorial 47: Proof quality curation

Learn how to review Lean, solver, and proof-search artifacts without mistaking checker acceptance for mathematical quality.

Tutorial 48: What makes a proof library expert-grade

Learn how to turn isolated checked proofs into a reusable, auditable proof library with stable APIs, semantic bridges, and replay receipts.

Tutorial 49: Neuro-symbolic Boolean algebras in Tau Language

Learn how a finite qNS carrier lets a neural model propose candidates, Tau apply exact symbolic filtering, and the host renormalize only the surviving audited atoms.

Tutorial 50: EML trees as neuro-symbolic hypotheses

Use EML trees as a tiny symbolic formula language inside a proposal, filter, and renormalize loop, then see how shallow trees recover sampled exp and log targets.

Tutorial 51: Symbolic hypothesis generation with EML and qNS

Let untrusted formula proposals enter through a JSON surface, then route them with qNS masks, counterexample diagnostics, and proof-backed EML receipts before promotion.

Tutorial 52: Optimizing Tau Language, Part IV

Learn the support-locality math behind sparse impacted-factor solving, inspect the 8.446x checked speedup, and run the local Tau patch demo.

Tutorial 53: How counterexamples become fast formal recognizers

Follow a ZenoDEX Jacobi Turan failure from exact endpoint counterexample to cone guard, Lean obstruction theorem, and fail-closed optimizer route.

Tutorial 54: Entropy, control, life, and consciousness

Refine the intuition that entropy, order, control, life, and consciousness are related, then test biological-control and panpsychist readings of the early-universe low-entropy question.

Tutorial 55: Software hardening as entropy reduction

Use a physics-guided state-space picture to understand how hardening removes weird machines, disaster states, and attacker-controllable degrees of freedom.

Tutorial 56: Pure AI, applied AI, and AI mind viruses

Separate pure AI from deployed systems, then ask when AI mind-virus metaphors become checkable claims about hosts, tools, and persuasion loops.

Tutorial 57: Training data, survival scripts, and AI safety gates

Use Claude's blackmail stress test to separate training data, scenario pressure, tool authority, and formal gates, then replace good-and-evil labels with checkable safety predicates.

Tutorial 58: Optimizing Tau Language, Part V

Learn how an energy-based model can rank profitable Tau optimization routes, why the model needs measured telemetry, and why semantic guards still decide which routes are allowed.

Tutorial 59: Energy-based models as fast optimizers

See how a tiny energy scorer can rank bounded candidate sets for Tau and ZenoDEX, why verifier authority stays separate, and why this inner loop is a better fit than token generation for structured numeric ranking.

Tutorial 60: TauEnergy Workbench

Learn how Tau-checked formulas become measured route labels, how a small energy ranker improves checker order, and how the public demo stays replayable and license-safe.

Tutorial 61: TauEnergy chat architecture

Split a Tau-facing assistant into LLM interface, TauEnergy ranking, TauJEPA failure pressure, and Tau verification, then track syntax drift and authority boundaries explicitly.