TYLER ROOST · INDEPENDENT RESEARCHER · SAN DIEGO
TimeLordRaps
Auditable AI · formal tools · interactive media
I build auditable AI systems, formal tools, and interactive media, turning ambitious ideas into inspectable, reproducible work. This page is the live instrument panel behind my GitHub profile: the contribution graph is the clock, the clock is a game, and the graph folds into a cube that solves itself.
Click or press Enter to turn the activity graph into the current time in your time zone. While the clock is showing, the contributions on the right fold into a Rubik's cube that scrambles and solves itself; drag it to orbit. Move the pointer over the court to steer a paddle in the game of Pong played between past and future, or use W and S and the arrow keys.
INSTRUMENT BAY
Everything here runs on time
Every instrument reads the same clock, so the time machine above moves all of them together. The cube lab is the exception: it keeps real time and re-scrambles on the twenty-second mark for everyone at once.
FEATURED WORK
Mechanisms you can inspect
Auditable AI and verification, formal and mathematical systems, and creative technology that makes difficult ideas tangible.
Verifier
Implements the Verifier Standard (VSTD) for portable, bounded, refutable computational evidence and provenance graphs.
Lean4 Explainer
Builds navigable proofsites from Lean 4 code using an explanation layer designed for higher-order specificity.
Hyperfields
Provides a Lean 4-checked, source-pinned map of the public hyperfield ecosystem.
Hypermath
Develops a formal universe from one primitive operation, with a Lean translation and explicit open proof obligations.
Ordinatics
Explores exact ordinal arithmetic and bounded typed satisfaction in an ordinal-first computational framework.
All repositories
Everything else, newest first, orbiting in the orrery above.
GITHUB.COM/TIMELORDRAPS →
WORKING PRINCIPLES
Evidence before confidence
- Evidence before confidence.
- Reproducible artifacts before broad claims.
- Open obligations and unknowns stated plainly.
- Ambitious ideas paired with mechanisms that can be inspected, tested, and challenged.
SUPPORT THE WORK
I publish open research, tools, experiments, and documentation across AI, computation, mathematics, and creative systems. If that work helps you think, build, or verify something more effectively, sponsorship helps fund more of it.
Sponsor on GitHubListen on SoundCloudFollow on GitHub
For a project-specific question or collaboration idea, open an issue in the relevant repository with a concrete use case, counterexample, or proposal.