かんたんに言うと
数学の証明をコンピュータに検証させるための言語です。書いた証明に穴があれば機械が指摘してくれます。
もう一歩くわしく
定理証明支援系と呼ばれる種類のソフトウェアで、数学の論証を機械が一段ずつ検査できる形式に書き下します。人間の査読より厳密で、正しいと機械が認めた証明には論理の飛躍が残りません。OpenAIのナビエ・ストークス方程式に関する公開物にこの形式証明が含まれていたことが話題になり、AIが出した数学的主張をどう検証するかという議論の中心に位置づけられています。
この用語が出てきたニュース