扱われている問題は、Sipserの『計算理論入門』に由来します：アルファベットが3ビット列の言語Bが正則であることを証明することです。文字列Bに属するためには、各行を2進数として読んだとき、下段の行が上段の2行の合計となる必要があります。たとえば、列の文字列[0,1,1][0,0,1][1,0,0]は、2進数で3+1=4となるためBに属しますが、[0,1][0,0][1,1]は1+0≠3となるため属しません。言語が正則であるとは、ある決定的有限オートマトン（DFA）がその文字列を exactamente 受理することを意味し、つまり入力長に関わらず固定されたメモリのみで認識できるということです。
解決策は、Bそのものは固定されたメモリでは左から右へ直接認識できないが、その逆言語B^Rは認識できるという洞察を利用しています。右から左へ（下位ビットから先に）文字列を処理することで、機械は二進法の加算におけるキャリーのみを追跡すればよいとなります。この加算DFAは3つの状態を持ちます：Carry 0（開始状態かつ受理状態であり、オーバーフローがないことを示す）、Carry 1（保留中のキャリーを示す）、およびDead（x_i + y_i + carry_inの期待値と合計ビットが一致しないときに入るシンク状態）です。遷移は3ビット列のシンボルでラベル付けされ、実線の矢印は合計ビットが正しいことを示す有効な遷移を、破線の赤い矢印は合計ビットが一致しない遷移を示し、Dead状態へと導きます。たとえば、Carry 0から列(1,1,0)、(1,0,0)、(0,0,1)を読むと、Carry 1を2回経由して受理状態のCarry 0に到達し、これにより逆転した文字列がB^Rに属し、したがって元の文字列がBに属することが確認されます。逆に、Carry 0から始まる文字列(1,0,1)、(0,0,1)は、最初の列後もCarry 0のままですが、2列目で0+0+0の合計ビット0が入力の1と一致しないためDead状態に遷移し、文字列を正しく拒否します。
このアプローチは、Mathlibの正式言語とDFAのライブラリを使用してLeanで形式化されました。証明は3つの調整されたコンポーネントからなります：アルファベットΣ₃上の集合ビルダー表記による言語Bの正確な仕様；状態、遷移関数、受理条件を定義する加算DFAの実行可能な実装；そして、オートマトンのキャリー状態と算術的合計を結びつける実行不変式を確立することにより実装が仕様に適合することを証明するものです。Mathlibは、正則言語が逆閉じているという定理などの重要なサポートを提供し、これによりB^RがDFAによって認識されることが示され次第、Bが正則であると結論づけることができます。このエンコードは、定理証明器における構成的証明がソフトウェア開発をどのように反映するかを示しており、仕様は要件に、実装はコードに、検証証明はテストスイートに対応し、ソフトウェアエンジニアに形式証明のメカニズムへの具体的な洞察を提供します。