Виталик: новая высокоуровневая языковая программа, которую стоит попробовать, должна облегчить чтение определений и теорем

Сообщение ChainCatcher, Виталик на платформе X заявил, что стоит попробовать новый тип "высокоуровневого языка программирования", который компилируется в Lean (или HOL и т.д.), с акцентом на то, чтобы сделать определения и теоремы как можно более понятными для человека. Не для доказательства, потому что доказательство должно быть просто правильным, ключевым является само определение и теорема. Предполагаемое использование заключается в том, что ИИ выводит большой объем доказательства, а читателю необходимо как можно легче понять, какие точные утверждения были фактически доказаны в этих выводах.