4 ms·

Loved it up until the introduction of proofs. Still can't wrap my mind around it. I'm beginning to think it's because "proofs" don't prove anything, they are ju

Loved it up until the introduction of proofs. Still can't wrap my mind around it. I'm beginning to think it's because "proofs" don't prove anything, they are just an argument that someone might find convincing.

tutfbhuf 3y ago
A computer program can also be considered a form of constructive proof. One may be confident that the program functions as intended until a bug is discovered. This is why theorem provers have such a strong type system, which reduces the likelihood of bugs compared to mainstream programming languages. However, it is important to note that bugs may still be present, just as they can be found in formal proofs on paper.
- quasarj 3y ago
  Do they have a strong type system? Maybe I just haven't gotten to that. My issue is that, there doesn't seem to be any rules for "evaluating" a proof to see if it is valid. Everything seems subjective? Maybe I'm just missing something. But coming from programming, I'm obviously used to a situation where I can put my code through a mechanical evaluator which will tell me if it works. Or at least, will tell me if the syntax is right!
  - lying4fun 3y ago
    When you proove something you are esentially prooving that a statement logically follows from some other statement(s) for which we know that are true You can evaluate the validity of a proof by checking the truthfulness of every statement which was used to argue that the proof holds Miniature example of a proof with relaxed rigor: Proove that 3+0=3 Proof: The above statement is a direct consequence of the additive identity axiom which states that x+0=x, if x is a real number. So the only thing we need to check is if 3 is a real number, and we know that it is. The statement holds, end of proof So to check the validity of this proof you could check if that axiom really exists and check if 3 is a real number, if some of those is false than the proof is invalid Edit: Or imagine that you have a DB full of axioms, theorems, prooven statements which you can use to proove a given statement. Then you could proove something by just referencing those. Eg. in the example above lets say that the neutral identity axiom has id 3, and the fact that 3 is a real number has an id 103. Then I could just say since 3 and 103 3+0=3
bo1024 3y ago
Proofs as usual written are informal summaries, but they are supposed (in today's age) to be linked to a very rigorous series of steps more precise than a Haskell program. Actually, it's very similar to the execution of a Turing Machine (there are formal connections): * There is a finite set of logical rules. For example, one rule is that if A => B and B => C are true, then A => C is true. * We start with a finite set of given facts. * At each step, we state a new fact and note it is true by combining previous facts with a rule. * At the end, we have the claim we started with. Example: prove 14 is an even number. 1. If a number equals two times an integer, it is even (given fact). 2. 7 is an integer (given fact). 3. 14 = 2 times 7 (laws of multiplication). 4. 14 = 2 times an integer (combining (2) and (3)). 5. 14 is even (combining (1) and (4)). At a more complex level, e.g. proofs by induction are often no more than programs with for loops.
- __rito__ 3y ago
  Love your comment. What are your favorite Math and Programming books?
  - bo1024 3y ago
    Lots of favorite math books! Not as many programming. Maybe I'd recommend Sipser's Intro to the Theory of Computation?
    - __rito__ 3y ago
      Already read most of it. Any lists for favorite Math book that you put together?

tutfbhuf 3y ago

A computer program can also be considered a form of constructive proof. One may be confident that the program functions as intended until a bug is discovered. This is why theorem provers have such a strong type system, which reduces the likelihood of bugs compared to mainstream programming languages. However, it is important to note that bugs may still be present, just as they can be found in formal proofs on paper.

quasarj 3y ago
Do they have a strong type system? Maybe I just haven't gotten to that. My issue is that, there doesn't seem to be any rules for "evaluating" a proof to see if it is valid. Everything seems subjective? Maybe I'm just missing something. But coming from programming, I'm obviously used to a situation where I can put my code through a mechanical evaluator which will tell me if it works. Or at least, will tell me if the syntax is right!
- lying4fun 3y ago
  When you proove something you are esentially prooving that a statement logically follows from some other statement(s) for which we know that are true You can evaluate the validity of a proof by checking the truthfulness of every statement which was used to argue that the proof holds Miniature example of a proof with relaxed rigor: Proove that 3+0=3 Proof: The above statement is a direct consequence of the additive identity axiom which states that x+0=x, if x is a real number. So the only thing we need to check is if 3 is a real number, and we know that it is. The statement holds, end of proof So to check the validity of this proof you could check if that axiom really exists and check if 3 is a real number, if some of those is false than the proof is invalid Edit: Or imagine that you have a DB full of axioms, theorems, prooven statements which you can use to proove a given statement. Then you could proove something by just referencing those. Eg. in the example above lets say that the neutral identity axiom has id 3, and the fact that 3 is a real number has an id 103. Then I could just say since 3 and 103 3+0=3

bo1024 3y ago

Proofs as usual written are informal summaries, but they are supposed (in today's age) to be linked to a very rigorous series of steps more precise than a Haskell program. Actually, it's very similar to the execution of a Turing Machine (there are formal connections): * There is a finite set of logical rules. For example, one rule is that if A => B and B => C are true, then A => C is true. * We start with a finite set of given facts. * At each step, we state a new fact and note it is true by combining previous facts with a rule. * At the end, we have the claim we started with. Example: prove 14 is an even number. 1. If a number equals two times an integer, it is even (given fact). 2. 7 is an integer (given fact). 3. 14 = 2 times 7 (laws of multiplication). 4. 14 = 2 times an integer (combining (2) and (3)). 5. 14 is even (combining (1) and (4)). At a more complex level, e.g. proofs by induction are often no more than programs with for loops.

__rito__ 3y ago
Love your comment. What are your favorite Math and Programming books?
- bo1024 3y ago
  Lots of favorite math books! Not as many programming. Maybe I'd recommend Sipser's Intro to the Theory of Computation?
  - __rito__ 3y ago
    Already read most of it. Any lists for favorite Math book that you put together?