Ideas you can read, try, and question.

State machines, abstraction, counterexamples, CEGIS, and the boundaries between heuristics and proofs. Start inside a card counter's head, then zoom out.

Why some "different abstractions" are the same thing in different clothes, and how to move problems into better toolchains.

Read and write small executable specifications by listing invariants first, then letting a solver produce behaviors that satisfy them.

Why internal models are more than prediction, why test-time learning is powerful, and why invariants matter when the model can drift.

Start from arcade, ATM, and vending-machine intuition, then compress those shared shapes into states and invariants.

Build Presburger arithmetic from zero and successor, and see why excluding multiplication makes every question decidable.

Compare proof by exhaustive search with sum-over-histories, then extend to action, weighted futures, and intelligent planning.

Use seL4 to study how small components can be proved and combined under checked assumptions.

Put logical refutation and Popperian falsification side by side. Separate proof in a closed formal world from corroboration in an open empirical one.

If consciousness is a nontrivial semantic property of computation, then no general Turing-machine detector can decide it from arbitrary encodings.

Recover missing requirements from witness structure, observation quotients, and minimal separator policies.

Learn branch exploration as witness search: concrete execution gives one real path, symbolic path constraints steer the next run.

Generate inputs from a grammar so more test cases reach the program behavior you want to inspect.

Define Church synthesis, examine which questions are decidable, and use smaller subproblems and invariants to manage complexity.

What separates a proof that checks from a proof that communicates, and how to curate a proof library for reviewer trust.

The difference between a collection of checking proofs and a library that an expert reviewer can navigate, trust, and extend.

Why the clopen algebra of Cantor space is the unique countable atomless Boolean algebra, and what its completion adds.

Read the Boolean algebra behind TABA step by step, including formulas for quantifier elimination and guarded successors.

Pointwise revision, fixed-point semantics, runnable demos, and the boundary between this prototype and full TABA tables.

Choose an optimization method according to the formula fragment, using BDDs and CNF where the required checks pass.

Explore LTL operators over bounded time horizons in Tau, the reasons those formulas are decidable, and ways to optimize them.

Search for faster rewrites and accept a candidate only when its certificate passes a trusted checker.

Detect blowup risk before solving, compress unused variables, and use route prediction without replacing proof certificates.

Ohad Asor's upstream Tau LTL(ABA) design, compared to the bounded Temporal Tau fragment.

Translate a governance sentence into a counting formula with two variables, then prove the translation is sound.

Model a bounded game between two players as a Tau table. Inspect the winning regions and the limits of the result.

Connect neural proposal distributions to Boolean constraints in Tau and test the conditions under which the connection holds.

Use EML trees to generate, rank, and test symbolic hypotheses. Examine what the bounded tests establish and which claims require a proof.

Generate symbolic hypotheses from EML trees and quotient networks, then verify them against bounded Tau specs.

Sparse impact factor solving: identify which variables actually matter for a given query, and skip the rest.

Energy-based route telemetry: measure which optimizer routes work, and feed the measurements back into route selection.

A tiny energy scorer ranks bounded candidate sets for Tau and ZenoDEX. Verifier authority stays separate.

Use formulas checked by Tau to measure optimizer routes and train a small ranker. Repeat the demo to check how the ordering changes.

Connect an LLM interface, TauEnergy ranking, TauJEPA analysis of failures, and Tau verification in one assistant.

Assess engineering by the experience it creates for the user, how the software behaves, and the evidence supporting it.

How entropy reduction connects living systems, computational systems, and the boundary where consciousness might enter.

Use entropy reduction as an analogy for hardening software. Examine how enforcement, tests, and proofs help address possible failures.

What survives into a trained model, what does not, and how safety gates at training time differ from gates at inference time.

Learning, whether in animals, humans, or AI, is the process of adjusting behavior probabilities based on reward signals. Those reward signals are set by a market for behaviors. Five layers: behavioral spectrum, incentive map, market, training as compression, alignment as market design. With an interactive lab.