Ethereum co-founder Vitalik Buterin has suggested the development of a new high-level programming language aimed at enhancing the readability of AI-generated proofs. This language would compile to theorem proving systems like Lean and HOL, focusing on making "definitions and theorems" more understandable rather than the proof process itself. The goal is to enable humans to clearly comprehend what AI-generated proofs have formally established, facilitating easier examination and verification of mathematical and logical claims.