3 ms·

Nope. With proof systems you have to convince the software. With traditional mathematics you have to convince a group of peers. Unless of course you consider i

• bmitc 3y ago
  I didn't say it was the same social social process but still a social process. Software is written by humans. Proof systems are not impervious to mistakes or issues. The point is that it is just another way to help augment normal proofs. The writers of the proof systems need to convince themselves and others that they have imolemented and tested things properly. Someone writing a proof in such a system needs to convince others that they have translated the proof correctly and used the system appropriately. For example, the below article describes a very social process to writing down a Lean proof of a theorem: https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ https://www.quantamagazine.org/lean-computer-program-confirm... > Unless of course you consider interacting with software to be “social”. Yes, but not in the way you imply. When you write software, you are writing for other humans and thus communicating to other humans. The fact that a computer can perform a task based upon what's written is basically just the cherry on top and not the whole cake.
  • deterministic 3y ago
    Fields Medalist Peter Scholze does not agree with you: https://www.microsoft.com/en-us/research/project/lean/ https://www.microsoft.com/en-us/research/project/lean/ “Lean has already demonstrated its potential to revolutionise and radically accelerate mathematics, for example, helping Fields Medalist Peter Scholze confirm a new theorem in the Liquid Tensor Experiment.”