ADV-050 · evidence animation · bridges
Cristian Guerra · QA Automation · Medellín, Colombia · @criguex
From OpenAI's theorem to Clay's text
OpenAI proved a formal statement; Clay's problem is a text. Lean bridges, one per clause, show that OpenAI's theorems imply Clay's (C) and (D) as written literally in Lean.
How to read this animation: Top: the three layers. Middle: every bridge row, colored by its recorded status in clay-lean-bridges.md. Bottom: the four K1 theorems and their axioms. Relative to ClayLiteral, which nobody independent has reviewed yet; no mathematician has reviewed the bridges.
Accessible explanation, equations, and source records
Open the evidence animation gallery · Download standalone HTML