4 ms·

This just seems like a native advertisement for Lean...

• DoctorOetker 7y ago
  I am not that perturbed by whatever framework they use, tools to translate the bulk of the majority of proofs from Lean to MetaMath to [...] and back will be made, the more important thing is that the number of humans aware of the existence of this tech and the more actually use it the better society will be off in the long run the following may seem totally impossible today but seems a lot less impossible to people who have been thinking about this for a long time: once sufficient mathematics has been translated, people can start adding physics postulates, one most physics has been inserted we can start formally verifying (up to validity of postulates on top of axioms) not just proper operation of digital circuits etc but also power plants and so on, and once interacting with proof systems becomes as widespread as alphabetic literacy, people might one day be able to formalize and vote on their requirements of society and policy, see predicted perverse incentives, or decide that policy can only be enacted when facets of their consequences can be proven. We might one day not vote on promises of strategy, also not vote on strategy, but rather on outcomes! I know it sounds absurd.