しかし、LLMが数学者にとって有用な検証可能な証明を生成できるようになったのは、ごく最近のことです。ソフトウェア検証やハードウェア検証において、ある程度の検証が可能になり始めています。

しかし、今後数年間のトレンドを予測すると、流れが一変する可能性もあると思います。形式手法、つまり形式検証や証明可能ソフトウェアといった分野全体です。これはプログラミング言語などの理論的な部分の、奇妙でほとんど辺鄙な領域であり、しばしば非常に学術的な色合いを帯びています。もっとも、DARPAのプログラムで証明可能な安全性を備えたクワッドコプターヘリコプターなどが開発されましたが。