>ask a math who completed his undergrad if he knows what modus ponens is
>"Nope"
>What about sequential calculus / basic symbolic proof?
>"No"
>show him a basic example of the use of basic inference rules
>he says he never encountered this
Are math programs really this shitty? Should I stay in CS? How the fuck do math undergrads do proofs if they don't even know what they mean and correspond to?
>formal symbolic proof
Yes, your kind should stay in CS away from the rest of us.
>he thinks proofs correspond to modern inventions of formal logic theory and not vice versa
You're a CS student, alright.
It is shit. Math should be done on your own, if you want to go out there to learn something learn Physics, or CS, which implies empiric knowledge. Just ignore the modern math, it is shit.
>>7683294
Without math science would basically rely on divination.
Stay in CS, it's the purest form of love. Also math.
>>7683205
Only retards aka CS majors would think you study formal symbolic proofs because its more rigorous than regular ones and not because it simplify proving statements about "proofs".
>>7683248
People really don't learn about this stuff in math programs? So what they just learn to solve really complicated formulas?
Set theory and the foundations of math are much more interesting than that.
>>7683299
>proof with formal verification
>hand wavy mathematician "proof"
pick one
>>7683248
>ZFC
>C
>he thinks choice is a necessary or sufficient axiom
>he doesn't know V equals L
>>7683307
Automated proving is impossible. Bitch all you want but no one is going to write proofs in source code. You're just going to need to understand them.
>>7683300
They do but it's not a requirement like abstract algebra, analysis, and topology.
>>7683313
Do you even univalent foundations?
>>7683205
>CS student talking shit about Pure Mathematics programs
Please tell me you are a memer from reddit or something. No one can be this fucking retarded.
>>7683313
>he cant into mu calculus
>>7683308
V=L is just as independent as choice.
>>7683593
No, V=L -> choice but choice -/-> V=L
>he doesn't prove stuff rhetorically with metaphors
>>7684465
Just like the swallow that dances in the morning sky, you are a fag
>>7684468
My dick is your mother's medication, she eats it every day.
To show the might of my metaphorical reasoning, I will prove the Banach fixed point theorem.
Let (X, d) be a complete metric space and f: (X, d) -> (X, d) a contraction. Then there exists a unique point x' in X such that f(x')=x' and that the sequence (x_n)_n, where x_n=f(x_(n-1)), converges to x' for all x in X.
If a paper is folded, all the points drawn on it get closer and closer to each other. When repeating this infinitely many times, only one point can remain fixed or the paper can not be folded, hence the fixed point is unique if it exists. Since all the points get closer to each other and only one point can remain fixed, folding after the infinite process can not change anything, so the final point is the fixed point and the sequence of folds converges to this point, for all x in X.
This is why companies hire CS grads as logicians instead of mathematkek majors.
>>7683313
Metamath.org
>>7683205
You asked a retard, and you asked a retard because you associate with retards. You're probably a fucking retard.
>>7684468
That's a simile bruv.
>>7683205
Math people don't use terms like "modus ponens" or "modus tollens". They don't even use terms like conjunct, disjunct, biconditional, etc... They do write logical statements and they do use the same methods but they don't know they are doing it. The majority of math people write their math in English prose as well. This isn't all that bad though since much of mathematics relies on second order logic and formal derivation isn't really that much more useful than the informal way math people do it.
In Comp Sci things are different though since people are ultimately only interested in computable functions and at most countably infinite sets. In other words, while math people are stuck talking about models of an axiomatic system, the CS people are able to talk about the systems themselves.
I agree though, undergrad mathematics programs should throw out garbage non-math shit like statistics and replace it with mathematical logic.
Curry-Howard isomorphism literally changed my life
>>7686651
>They don't even use terms like conjunct, disjunct
Because only CS majors and Philosophers desperate to make their fields sound complicated use obfuscated sesquipedalian terminology like that. There's nothing wrong with calling logical operations AND, OR, and XOR.
