本文所讨论的问题源自Sipser的《计算理论导论》：证明语言B是正则的，其中B由三位列的字母表上的字符串组成。当每行被读作二进制数时，如果底行等于顶部两行的和，则该字符串属于B。例如，列字符串[0,1,1] [0,0,1] [1,0,0]属于B，因为二进制3+1=4；但[0,1] [0,0] [1,1]不属于B，因为1+0≠3。如果存在一个确定性有限自动机（DFA)恰好接受该语言的所有字符串，则该语言是正则的，这意味着识别仅需要固定内存，与输入长度无关。
解决方案利用了以下见解：虽然B本身无法在从左到右处理时仅用固定内存直接识别，但其反转B^R可以。通过从右到左处理字符串（先处理最低有效位），机器只需跟踪二进制加法中的进位。这个加法DFA有三个状态：进位0（同时是起始状态和接受状态，表示无溢出），进位1（表示有待处理的进位），以及Dead（当总和位与x_i + y_i + carry_in的预期值不匹配时进入的沉没状态）。转移由三位列符号标注；实线箭头表示总和位检查通过的有效转移，而虚线红色箭头表示总和位检查失败并转移到Dead状态的转移。例如，从Carry 0状态读取列(1,1,0)、(1,0,0)、(0,0,1)，会经过两次Carry 1并最终回到接受状态Carry 0，确认反转后的字符串属于B^R，因此原始字符串属于B。相反，字符串(1,0,1)、(0,0,1)从Carry 0开始，在处理第一列后仍保持在Carry 0，但在处理第二列时转移到Dead状态，因为0+0+0产生的总和位为0，而输入声称是1，从而正确地拒绝了该字符串。
此方法在Lean中使用Mathlib的正式语言和DFA库进行了形式化。证明由三个协调组成部分构成：使用字母表Σ₃上的集合构造器表示法对语言B进行精确规范；可执行的加法DFA实现，定义其状态、转移函数和接受条件；以及通过建立将自动机的进位状态与算术求和连接的运行不变量来证明该实现与规范匹配的证明。Mathlib提供了基本支持，包括正则语言在反转下封闭的定理，使得在证明B^R被DFA识别后能够得出B是正则的结论。该编码展示了定理证明器中的构造性证明如何镜像软件开发，其中规格对应需求，实现对应代码，验证证明对应测试套件，为软件工程师提供了形式验证机制的具体见解。