Lean
Leanは、数学の証明やプログラムの性質を形式化して検証する定理証明支援系であり、プログラミング言語でもある。
記事3本
最終言及 Leanは、Microsoft ResearchのLeonardo de Mouraが2013年に開発を始めたオープンソースの定理証明支援系であり、関数型プログラミング言語でもある。数学の命題と証明を形式言語で記述すると、証明の各段階をコンピューターが検証する。2023年からは非営利組織Lean FROが開発を主導している。
数学の形式化やソフトウェアの検証に使われ、コミュニティが整備する数学ライブラリmathlibが広く利用されている。AI分野では、モデルが生成した証明を機械的に検証する手段としても使われる。
この説明は、AIPOSTの記事と広く知られた事実をもとにまとめたものです。誤りがあれば訂正依頼でお知らせください。
この項目を扱った記事
5月27日の事案では、内部モデルがLeanを使う課題に取り組んでいました。
OpenAIは解析的な論文と、明示的な規則に照らして数学的議論を検証するシステム「Lean」で形式化した証明の両方を提示しました。