Formalization overview
Every definition, lemma, and theorem in this repository’s Lean formalization, generated from Gate’s own dependency analysis.
| Course | Modules | Declarations |
|---|---|---|
| Logic | 18 | 209 |
| Structure | 8 | 135 |
| Programming Languages | 0 | (no content yet) |
| Program Correctness | 0 | (no content yet) |
| Computer Networks | 22 | 312 |
| Computer Chips | 5 | 62 |
| Computer Systems | 0 | (no content yet) |
| Library | 5 | 185 |
Where the text comes from
Every piece of text on these pages sits in a box. The border of the box says who stands behind the text.
A gray border, with the letters AI in the corner, means the text and the mathematics inside it were written by an AI, with little human control. A machine has checked that the proofs are correct. A person has yet to read the words and agree with them.
A green border means a person approves of the text. An AI may still have written part of it. Approval means a person has read it and stands behind it.
A border in the colors of the electromagnetic spectrum, running from ultraviolet in the top left corner to infrared in the bottom right, is reserved. It is rare, and where it appears the text says why. It carries no claim about what deserves your attention.
Read every box with the same care. A border records who stands behind a text. Whether the text is right is yours to work out, and that stays true on every page here.
An experiment in control
This development is an experiment in getting AI under control. Mathematics and logic are the proving ground, and we’ll venture off in applications such as programming, correctness, computer networks, computer chips, and computer systems. Every formal claim here is checked by a machine, so a step that the proof checker fails to verify also fails to build. That gives the AI a hard boundary to work inside, and it gives a human a short list of things left to judge by hand. The borders make that list visible.
The spirit of the experiment is that of Edsger Dijkstra, in his interview Denken als discipline (Discipline in Thought). Dijkstra asks for a way of thinking that keeps a problem small enough for one mind to hold, and for proof rather than trust as the way to know that a program is right. The same discipline is what we ask of an AI here.