proof

∀ · specifications checked by a prover, implementations that follow them name for name, and data experiments with papers. The repository.

Preprints

• Contextual bandits as a verified specification
  A Z3 model of the decision layer, ported to Haskell
  Preprint v0 (draft, not peer reviewed) · November 2026
  PDF, English · source
• Time is a flat circle
  An essay on eternal return, from Nietzsche's demon to a theorem in Lean
  v0 (skeleton, not for circulation) · November 2026
  PDF, English · source
• Calm surface, fat tails
  Taleb's fat-tail diagnostics applied to the S&P 500, 1950 to October 2026
  Preprint v0 (draft, not peer reviewed) · November 2026
  PDF, English · source
• Who wins the slot?
  Forecasting audiences of big TV shows as a competition between channels: XGBoost, a neural network, Mistral Timestral and a joint competitive share model
  Preprint v0 (draft, not peer reviewed) · November 2026
  PDF, English · source

Contextual bandits

• Contextual bandits
  The contextual bandit: the idea, the files, what Z3 proves, the Haskell port
• Bandits contextuais
  The same page in Brazilian Portuguese
• Output of the video's code
  The video's experiments, as the Haskell port writes them
• 1. The contextual bandit is specified in Z3, not in Lean
  Why the specification moved from Lean to Z3
• Diagrams
  The archify diagrams of the bandit, in English and Brazilian Portuguese.

Z3 reports

• z3-scala: every Z3 check of this repository, in Scala
  Every Z3 check: the statements, how they are checked by refutation, the commands
• port-audit: Z3 checks of chaceon
  Audit of chaceon, the Rust port of WAVEWATCH III: 28 statements and the coverage table
• Triangle grids for spectral wave models
  Triangle grids for WAVEWATCH III: 13 statements on the size rules and the sub-step count

Video script

The first 1:30 of the script, with its subtitles and no voice (the roteiro-preview skill). Subtitles · shot list.

• Script: CMAB, A/B tests and RSI, in 30 minutes
  The contextual bandit, the A/B test and recursive self-improvement in an explainer video, with an invariant in Z3 or a function in Haskell behind each sentence
  v0, draft · 9 November 2026
  PDF, Português (BR) · source
• The video script: CMAB, A/B tests and RSI, in 30 minutes
  How the video script is written and built