[1/3] 书上一个不起眼的引理,卡了我一个半月,证明写了一千多行代码还没写到一半。然后其中有个关键步骤,又卡了我一个多星期,直到刚才才终于拨云见日,但要想完成它还要再写很多代码。形式化证明的繁重工作量,在一般情况下是无法避免的(少数情况下才可以自动推理)。
[1/3] 书上一个不起眼的引理,卡了我一个半月,证明写了一千多行代码还没写到一半。然后其中有个关键步骤,又卡了我一个多星期,直到刚才才终于拨云见日,但要想完成它还要再写很多代码。形式化证明的繁重工作量,在一般情况下是无法避免的(少数情况下才可以自动推理)。
No replies yet.