How the large finite computations behind the theorems are checked: by two independently written programs, and by a proof checked by machine. And what each layer guarantees, and what it does not.
This animation explains Section 9 and Appendix A of the paper Finite graph certificates for composite terms in rational floor sequences by Yuri Odagiri, together with its supplement: the eight obligations of the finite computations, the two independent implementations and their element-by-element comparison, the Lean formalization (the kernel-checked certificate for 7/5, and the word-labelled pipeline for 5/2 accepted with native_decide), what the formalization does not cover, and how to reproduce everything. It follows the one-step method, word-labelled method and waiting times, limits and open problems videos.
The Lean code on screen is quoted verbatim from supplement/lean. The axiom dependencies shown are those reported in the paper; the repository does not contain a transcript of the #print axioms output. As the paper’s acknowledgments state, the mathematics, the programs and the Lean formalization were produced by AI systems, and the paper has not been independently reviewed by human mathematicians; the author asks readers to check it.
The narration was generated with Gemini 3.8 Flash TTS and plays in sync with the captions. It starts in a window-filling view; W switches to the page view with the chapter list, and F uses the whole screen. If the audio file cannot be loaded (for example when the HTML file is opened on its own), the browser's speech synthesis reads the captions instead.
Paper: DOI 10.5281/zenodo.22997709 · Sources and reproduction: github.com/ixixi/rational-floor-certificates · 日本語版 · The one-step method · The word-labelled method · Waiting times, limits, and open problems