It certainly is about those specific proofs and anything that has been rigorously proven in Lean. We’re discussing techniques that show something is correct forever, and those proofs show that something is correct forever. Philosophical arguments don’t even show that something is correct today. This is why the examples I gave earlier are now not explained by philosophy but by other systems. Once the tooling exists to lift a discussion out of philosophy, that is the end of philosophical debate for that topic.
Furthermore, the kernel still relies on CPU, memory and OS behavior to be bug free.
Only to a point, just like human language proofs require the reviewers brains to be bug free to a point. The repeated verification makes proofs as correct as anything can get.
just like human language proofs require the reviewers brains to be bug free to a point. The repeated verification makes proofs as correct as anything can get.
Exactly, I’m glad you understand. There’s no epistemological certainty in math, just like in normal language. We have to make do with being pretty certain, as good as it gets. I like lean for it’s intended purpose: advancing math. No one involved in lean is seriously claiming it produces some kind of religious absolute certainty. Neither is anyone trying to replace philosophy.
Math can’t elevate anything above philosophy, because in a sense, it is part of philosophy, one of the parts using specialized language, specifically the part that is concerned with tautologies.
Have you clicked on the links to the philosophy wiki I provided? Maybe read about what a brilliant mathematician and philosopher has written on the philosophy of mathematics to convince yourself, that philosophy of mathematics is valuable and necessary (wether you agree with his specific point of view or not). You’re already engaging in philosophical debate yourself. Your claims about the nature of philosophical arguments and mathematical proofs are themselves philosophical in nature.
Also, though you haven’t clearly articulated your philosophical position, it seems to be close to the one of the famous Vienna Circle
, which was inspired by Wittgenstein, but later rejected by him. It’s generally agreed today, that their project of logical empiricism has failed. You can find the critiques of the various points in the article above.
It certainly is about those specific proofs and anything that has been rigorously proven in Lean. We’re discussing techniques that show something is correct forever, and those proofs show that something is correct forever. Philosophical arguments don’t even show that something is correct today. This is why the examples I gave earlier are now not explained by philosophy but by other systems. Once the tooling exists to lift a discussion out of philosophy, that is the end of philosophical debate for that topic.
Only to a point, just like human language proofs require the reviewers brains to be bug free to a point. The repeated verification makes proofs as correct as anything can get.
Exactly, I’m glad you understand. There’s no epistemological certainty in math, just like in normal language. We have to make do with being pretty certain, as good as it gets. I like lean for it’s intended purpose: advancing math. No one involved in lean is seriously claiming it produces some kind of religious absolute certainty. Neither is anyone trying to replace philosophy.
Math can’t elevate anything above philosophy, because in a sense, it is part of philosophy, one of the parts using specialized language, specifically the part that is concerned with tautologies.
Have you clicked on the links to the philosophy wiki I provided? Maybe read about what a brilliant mathematician and philosopher has written on the philosophy of mathematics to convince yourself, that philosophy of mathematics is valuable and necessary (wether you agree with his specific point of view or not). You’re already engaging in philosophical debate yourself. Your claims about the nature of philosophical arguments and mathematical proofs are themselves philosophical in nature.
Also, though you haven’t clearly articulated your philosophical position, it seems to be close to the one of the famous Vienna Circle , which was inspired by Wittgenstein, but later rejected by him. It’s generally agreed today, that their project of logical empiricism has failed. You can find the critiques of the various points in the article above.