Ciro Santilli @cirosantilli 37

This tutorial has the merit of actually trying you to do some meaningful mathematics before teaching you a billion items of syntax and dependent type theory nuances.

It is quite the beauty of mathematics beautiful that with exponentiation, even if you take relatively small numbers of the order of 100 then:is already equal to the number of atoms in the universe.

All competitors run on the same hardware which is cool. One of their challenges then would be how to balance CPU and GPU, given that as of 2025 Stockfish uses CPU and Leela Chess Zero uses GPU.

Alternative to set theory, and some say it is better for proof assistants, and many of the most popular proof assistants of the 2020s use it e.g. Lean and Coq.