CRM Colloquium by Terence Tao: "Machine Assisted Proofs"

[@robfielding8566]

I am in the process of learning Lean4. Only a few days ago, Dependent Type Theory really started to sink in; and I read the book by Simon on Type Theory. I think once I get fluent in doing theorems, it will be useful. This could be a good language for writing compilers. Maybe theorems can make it into mainstream programming languages.