Question
In October 2024, Kevin Buzzard will begin a five-year project to formalize an instance of this task as part of the Xena Project. Calc, term, conv, and tactic modes are used to verify this task with the software Lean, a competitor of Coq (“coke”). “W·L·O·G” is used to justify arbitrary choices in this task. Appel and Haken checked 1,834 (*) cases in the earliest significant instance of using computers for this task. A method or example is provided by constructive instances of this task that may be performed via exhaustion, induction, or contradiction. This task is performed in two columns with statements like “S·A·S” and “SSS” in typical geometry curricula. For 10 points, name this task of demonstrating a mathematical truth. ■END■
ANSWER: proof-writing [accept equivalents, like proving a mathematical statement; accept word forms of formal proof or proof verification or proof verifier or proof assistant or theorem prover or computer-assisted proof or proof by exhaustion or proof by induction or proof by contradiction] (Kevin Buzzard received a million-pound grant to formalize Fermat’s last theorem in Lean.)
<David Bass, Science - Math> ~27340~ <Editor: David Bass>
= Average correct buzz position
Buzzes
Summary
| Tournament | Edition | Exact Match? | TUH | Conv. % | Power % | Neg % | Average Buzz |
|---|---|---|---|---|---|---|---|
| 2024 PACE NSC | 06/08/2024 | Y | 36 | 100% | 36% | 0% | 76.89 |