TechFlow news, July 21, according to Vitalik Buterin (@VitalikButerin) in a post, he suggested developing a new type of high-level programming language that can be compiled into Lean (or formal verification tools such as HOL), with the core goal of making it as easy as possible for humans to read definitions and theorem content (rather than the proofs themselves). The envisioned use case is: AI is responsible for outputting proof content, while the language helps readers quickly understand the specific propositions proved by AI.
Add to Favorites
Share to Social Media
