Lean proved this program was correct; then I found a bug. 13 Apr, 2026 lean formal_verification security fuzzing I fuzzed a verified implementation of zlib and found a buffer overflow in the Lean runtime. AI agents are getting very good at finding vulnerabilities in large-scale software systems. Anthropic, was apparently so spooked by the vulnerability-discovery capabilities of Mythos, they deci
こんにちは、チェシャ猫です。 先日開催された BuriKaigi 2026 で、定理証明支援系 Lean を用いたコンパイラの証明について登壇してきました。公募 CFP 枠です。 fortee.jp 講演概要 近年、生成 AI を利用したシステム開発はもはや特殊な選択肢ではなく、一般のプログラマでも十分に活用しうる水準の技術となりました。一方、生成 AI が高速かつ大量に、しかしハルシネーションを含んだ出力を行うことにより、その正しさを改めて確認する側の人間の負担感も様々な場所で聞かれ、AI Slop などと呼ばれています。ちなみに Slop とは「泥水」のことで、低品質な出力を例えた表現です。 今回の講演では、このような状況に対して「検証可能な仕様記述」が重要になるのではないか、という洞察を出発点とします。すなわち、記述として曖昧性を持たず、実装がその仕様を満足しているかどうかが明確かつ
2026.01.01 Leanによる形式化は、長期的な検証や説明責任を可能にする記録装置となり得るか？ カテゴリ：研究関連の現状報告 昨年後半のLean関連活動 前回の記事では、定理証明支援系ソフトLeanに関連した活動が昨年後半、（私を含め）私の周辺において益々活発になっていることについてご報告しましたが、今回の記事では、少なくとも私の現在の認識において、このような活動に関わることにどのような意義があるかについて検証し、解説していきたいと思います。 ただし、誤解がないように明記しておきますと、「活動に関わる」と言っても、私自身はこれまでそういう計算機のプログラミングの世界とは
Press ← or → to navigate between chapters Press S or / to search in the book Press ? to show this help Press Esc to hide this help Introduction Welcome to From Zero to QED, an informal introduction to formality in Lean 4. This article series teaches the language from first principles. Lean is expressive but the learning resources remain scattered and incomplete. This series is a best effort to fil
そろそろ懐が寂しいので終わりです。ご協力ありがとうございました！ Lean 4で作っている正規表現エンジンを、もっと便利で実用的なライブラリにするために、一緒に開発・証明してくれる仲間を募集しています。せっかくなので、今回はいくつかのIssueにバウンティを設定してみることにしました。 github.com Leanや形式検証に興味がある方、Unicode周りが好きな方、正規表現エンジンの内部に触れてみたい方ならどなたでも歓迎です。 取り組む Issue は自由に選べますし、実装方針の相談やレビューは気軽にどうぞ。必要なら背景説明や資料も用意します。 報酬について 対象 Issue を解決して PR がマージされたら1件につき10万円〜のバウンティをお支払いします。重めのタスクはマイルストーンに分けて途中支払いもできますし、難しい部分を突破したときの追加ボーナスもあります。 こんな方に向い
ご来店ありがとうございます。新刊発売予定のお知らせです。 2025年9月4日（木）、井上亜星著 『ゼロから始めるLean言語入門 ― 手を動かして学ぶ形式数学ライブラリ開発』の発売を予定しています。 書名にもある通り、本書はLeanという比較的新しいプログラミング言語の入門書です。プログラミング言語としてのLeanは、いわゆる関数型言語の仲間と言えます。 他の関数型言語、とくにHaskellを使ったことがあれば、典型的なアルゴリズムやデータ構造を扱うLeanのコードをなんとなく書けるかもしれません。その程度には「ふつうの言語」であるとも言えます。 しかしLeanには「ふつうの言語」にはない大きな特長もあります。具体的には、「数学の証明をソフトウェアとして形式化できる」あるいは「プログラムの挙動に対する証明ができる」という、定理証明系としての側面です。本書では、そのうち「数学の証明をソフトウ
28 Aug, 2025 This week I reached a milestone in my most useless side project so far. I finished writing a tic-tac-toe game in Lean 4, along with proofs to guarantee that the game behaves correctly! It “only” took me 20 hours, 1000 lines of code and endless suffering… Totally worth it, as you might expect. Chances are you haven’t heard about Lean before, so I’ll share more details below. But first,
Why Lean 4 replaced OCaml as my Primary Language 13 Aug, 2025 programming_languages code theorem_proving perspectives As I was reading Hacker News today, I happened to stumble upon an article titled "Why I Chose OCaml as my Primary Language". This was a particularly interesting read for me: over the past few years, I have been gradually transitioning1 my primary language away from OCaml to anoth
Types of Types: Common → Exotic Programming languages offer various ways to model data through their type systems. Let's explore these concepts using Lean, which has a particularly rich type system supporting four fundamental kinds of types: function types (Pi types), product types, sum types (inductive types), and quotient types. In Lean, mathematical objects exist in a three-level hierarchy: Uni
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
A Lean companion to “Analysis I”