Why do mathematicians not use real formal proofs?

>>8048956
> why do programmers not code everything in assembly

>>8048956
Umm... because they aren't autistic?

>>8048982
>math majors
>not the biggest autists

>>8048956
>CS majors are too stupid to recognize proofs as correct unless they're unreadable formal proofs

>>8048956
I guess this would help in long proofs

>>8049060
CS "major" here. Can affirm I hate it when you use natural language in your proofs.

Proofs can be hard to follow. They also need to be convincing. This is why we generally write them in prose or as a story. We walk people through a proof to explain it better. Reading a page of letters and symbols only is nonsensical for understanding. Part of it is also tradition.

>>8049065
I think in natural language and I write whatever I think. I don't see a problem. And I am a cs major(doubling with math though)

>>8049070
I have primary psychopathy and I can manage my mind much the way an AI would; at will. I think in algorithms and write in natural language purely as a communal habit. When I try to explain my highly algorithmic and logically refined thoughts and feels in natural language, people say it sounds vague.

Fuck natural language, seriously.

>>8049091
Autism

>>8048960
It's more like
>Typical rigorous math proof ~ really vague buggy pseudo code
>actual rigorous proof (I.e. what OP is talking about) ~ actual bugfree code

>>8049092
Pretty much, except I can control it intuitively.

>>8049108
You have no idea what you are talking about

>>8048960
Because compilers have a tendency to generate better code than humans.

Because informal proofs are just as valid. It is a matter of style not rigor.

>>8049123
>generate better code
No, it's because the higher levels of abstraction make it faster/easier to arrange algorithms. When you compile high-level languages, it tends to make awful code. We're just lazy enough to let Moore's law handle the loss in efficiency is all.

>>8049136
This is wrong

Compilers make a shitton of optimizations. Unless you're an Assembly god, don't care about your Assembly being human-readable and are ready to spend a fuckton of time optimizing, the compiler will beat you.

>>8049174
>optimizations
Yes, but it's never going to be fully optimized code.

The idea that a compiler will make better code is complete bunk. Compiler optimization is just about making up for the autistic code normally generated by a primitive compiler's algorithm.

>>8049174
This.

What is it so hard to understand about this, it is like /sci/ never get this.

Exactly same reason applies for why we use numerical methods even though it can be solved exactly.

>>8049174
That is not the reason why people use high level languages

>>8049056
Moth math majors don't end up being mathematicians though? It's pretty difficult for is pretty difficult for autists to succeed in academia.

>>8048956
http://arxiv.org/pdf/1501.02155.pdf
Some do.

>>8049202
True, and people used high-level languages long before compilers got this good

But it is false that you would typically get better performance by hand-coding Assembly than by writing it in C and enabling most optimizations

>>8049187
optimization nerds who have never seen literate code convince themselves that hand-optimized code is worth not accomplishing shit.

algorithmic complexity matters. sometimes a shitty runtime environment matters. hand-optimized code doesn't matter unless you're dealing with extremely specific hardware and being paid a lot of fucking money to bother.

Not to mention that JIT makes the compiler/VM win even harder now.

>>8049219
>algorithmic complexity matters
Is what I said: >>8049136

File: 1441567863512.jpg (444KB, 1280x1020px) Image search: [Google]

444KB, 1280x1020px

>coq is ready

>>8048956
We're writing maths, not logic.

>>8048956
1. Because mathematicians derive more insights from a proof than the fact that it is valid, and rigid proofs, especially from automatic provers, tend to be a clusterfuck.

2. Some areas are hard to formalize with axioms without going down to set theory, it's not an coincidence that most formal proofs are done for graph theory or transition systems.

3. You just push the problem "I trust that you didn't miss a case and I missed a mistake in your prose" to "I trust your proof system is sound and your implementation is correct".
Yes there are formal methods for the implementation stuff, then you have the problem "I trust that you specified the correct thing" and there are no case studies on verifying a whole system of the size of a theorem prover.

>>8048956
>clause function names
Pleb tier, no matter the language.

>>8049066
This is what retards who can't into logic actually think.

>>8049117
>I just didn't mention those details because you're supposed to be able to read my mind to know that those special cases are handled separately and aren't important to me because I'm only interested in these cases!!
Kek

>>8049124
It is a matter of rigor, not style. On what grounds can you call your proof rigorous when you're hand waving away so much material?

>>8048956
In 10 years the field will be dominated by AI mathematicians doing formal proofs.

>>8050397
The proofs themselves are less interesting than the methods developed, and I'd like to see the AI know which results are worth proving.

>>8050397
>>8050416
This just in: doing actual mathematics requires general intelligence.

>>8050501
I'm sure Garry Kasparov and Lee Sedol thought the same of their area of expertise as well.

>>8050527
Toplel. Please tell us more.

>>8049196
I thought numerical methods are mainly used because:
1)No closed form solution
2)Fucking floating point explodes, so iterative/implicit/whatever methods usually give much better results, compared to what you'd have got if you simply used direct formula.

>>8050501
>muh high emotional IQ

>>8050547
low iq brainlet found

>>8049123
>Because compilers have a tendency to generate better code than humans.
Compiler spods have been saying this for decades. It remains wrong. I was a fairly well remunerated consultant in the embedded software market, helping out companies who belately realised the compiled code was bloated beyond belief and would not fit into the limited resources, and also slow as treacle on a cold day.

>>8050669
Nice, why did you stop? What are you doing now?

Leaving out steps that are supposed to be obvious to the reader and trivial to prove is intended to make reading the proof easier. If everyone is familiar with a particular theorem there is no reason to include its proof in your proof, it just distracts the reader from the important parts. Furthermore programming is quite similar in that you usually have several layers of abstraction for the purpose of readability.