In search of falsehood
Opus 4.6 finds proofs of false in Rocq and Lean kernels.
Tristan Stérin's Blog
Blog posts by Tristan Stérin
Latest posts
Personal relationship with the bouba-kiki effect
Or a tale of two churches.
Opus 4.6 is great at formal proofs
Opus 4.6 is great at formal proofs in Rocq and Lean4.
BB(5) paper accepted to STOC 2026
Determination of the fifth Busy Beaver value.
BB(5) talk at Collège de France
The Philosophy of Mathematical Practice seminar.
Our molecular computer on bioRxiv
A Thermodynamically Favoured Molecular Computer.
6 Collatz tiles - base 3/2 follow up
Reading base 3/2 in Collatz tilings.
6 Collatz tiles
Assembling Collatz sequences using Wang tiles.