Якщо великі математичні моделі працюють (схоже, що поки що так і буде), буде дивно мати купу раніше нерозв'язаних теорем, доведених, тоді як цілком можливо, що немає людини, яка могла б прочитати докази моделі, щоб насправді знати, як працюють доведення

Це начебто вже так працює

@_joshd це може спрацювати, якщо модель підсумовувача також виробляє lean доказ, який типово ідентичний оригіналу