News for hackers. Stuff that matters.
Re:Why Mathematical Proof Is a Social Compact by GoblinSlayer on Friday September 01, 2023 @04:55AM (#37348342)
>If a program is accepted by the proof checker, then by construction it must be a valid mathematical proof.

Huh? How? Truth is an empirical fact, you can't possibly define it into existence.

Re:Why Mathematical Proof Is a Social Compact by paldepind2 on Friday September 01, 2023 @05:13AM (#37348461)
You have a point, but to be fair the person you replied to didn't use the word "truth". They said "valid mathematical proof". An in the context of type theory or formal logic "valid proof" is indeed something that has been "defined into existence" (in type theory "valid proof" ≈ "well-typed term"). Whether it represents "truth" is a different matter. Though such systems can (ideally) be proven sound in and with respect to "normal" mathematics. At that point I guess the "truth"ness depends on you overall belief in math :)
Re:Why Mathematical Proof Is a Social Compact by dagw on Friday September 01, 2023 @05:12AM (#37348456)
All mathematical "truths" are defined into existence as you call it. All mathematical proofs are essentially of the form If A Then B. B is only a "truth" since we defined A a certain way and accept it as True. Due to its very nature, there are no empirical facts in mathematics.

You can argue that the is no Truth is mathematics, which is a perfectly reasonable position to take.