vitalik.eth
@VitalikButerin
I choose balance. First-level balance.
mi pinxe lo crino tcati
Joined May 2011
549 Following 7.4M Followers
A new type of "high-level programming language" that seems really worth trying to make, is a language that gets compiled to Lean (or HOL, or...) that is specifically about making it as friendly as possible for a human to read definitions and theorems.
Not the proofs - as all that matters with proofs is that the proofs are correct - just the definitions and theorems.
The intended use case is that AI outputs a blob of proofs, and you're trying to make it as easy as possible for anyone reading the output to understand what the actual precise claims are that have been proven
Show more
