#формальная-верификация
-
F*: the programming language where proofs are built into the code
Developed by Microsoft Research, Inria and the community, the F* language combines functional programming with formal proofs. Its code already runs in Firefox, the Linux kernel and the Azure cloud.
-
A False “Refutation” of the Collatz Conjecture Exposed a Bug in Lean's Kernel
A soundness bug has been found in the Lean proof system's kernel: with the help of AI, a formally accepted but incorrect “refutation” of the Collatz conjecture was constructed. Lean's author, Leonardo de Moura, has published a breakdown of what happened.