那該怎麼辦？我一直在參與 LemmaScript 的工作。它是 TypeScript 的註釋版本，可以接收既有程式碼，例如 EtherCalc 與 SocialCalc 加起來大約 7 萬行的 JavaScript；我與試算表發明人 Dan Bricklin 共同維護這兩個專案。接著，我們可以開始撰寫不變量，把它們表述為附有密碼學憑證、可由 AI 智慧體證成的引理。