Der Mitbegründer von Ethereum, Vitalik Buterin, hat die Entwicklung einer neuen Programmiersprache auf hoher Ebene vorgeschlagen, die darauf abzielt, die Lesbarkeit von KI-generierten Beweisen zu verbessern. Diese Sprache würde in Theorembeweissysteme wie Lean und HOL kompiliert werden und sich darauf konzentrieren, "Definitionen und Theoreme" verständlicher zu machen, anstatt den Beweisprozess selbst. Das Ziel ist es, Menschen zu ermöglichen, klar zu verstehen, was KI-generierte Beweise formal festgestellt haben, um die Prüfung und Verifikation mathematischer und logischer Behauptungen zu erleichtern.