The maths is real.
You can check it.
People choose the questions. Tools help work through them. Explore mathematics, software, and art with the sources and assumptions close at hand.
Find a way into the work.
Agent Data Pod
A specification for storing agent memory and state in user-controlled Solid Pods. Read the protocol, examples, and implementation boundaries.
Questions, worked through
Published pieces, each one question worked all the way to the number. Which gemstone cut gives fire rather than cold sparkle. Why a curling stone follows its own rotation. What it takes for a bar to order The Gates of Hell in 96 hours.
Follow a question
Gemstones, curling, photonics, and more. Start with the question, then follow the references, assumptions, and evidence on each project page.
Find the move your proof needs
Polya brings human judgment and AI-assisted proof work into one workflow. A strategy states what it gives and needs. Lean checks the proof built with it. The prototype remains private.
Human judgment. Evidence you can inspect.
The campaign begins with Polya. Each other surface carries its own evidence.
Choose the question
People decide what matters and whether the mathematical statement faithfully describes it.
Show the check
A reproducible result names its artifact, revision, assumptions, and the command used to check it.
Keep the edges visible
An unfinished proof, an old measurement, and a missing check remain distinct states.
Tim Jacoby
Previously Engineering Director at Meta, where I led the team that shipped Meta Ray-Ban Display and built the avatar system for the metaverse platform. I spent a decade building products at the intersection of hardware, software, and human experience.
Now I make mathematics, software, and interactive art. Lean 4 checks proof terms. People remain responsible for the questions, statements, and interpretation.
Explore the work and follow the evidence at your own pace.
