Who Do You Trust More?

Created: · Last Updated:

You are Elon Musk. You are sending a calculator to Mars to build a city. The city construction solely relies on a 100-line program running on the calculator. You release the source code online, and seven different groups claim that the program is correct. Who do you trust more?

  1. Euclid, Newton, Euler, Gauss, Einstein, and Grothendieck work together and come up with a 5-page paper proof.
  2. Ten Ph.D. students, guided by Terence Tao, build an 100-line proof in Lean.
  3. Grok 42 xHigh generates a mechanized proof based on the most advanced type theory on Earth that only ten experts can comprehend the rules.
  4. A college student who has used this exact calculator for over a decade for every exam and never encountered a bug.
  5. Ten senior engineers check the code line-by-line. They are going to Mars with the calculator. If there is a bug, they die.
  6. You, Elon Musk, offered a $1 billion bounty to anyone who could find a bug. The bounty remains unclaimed for five years.
  7. Jesus Christ returns to Earth and says it’s correct.