Why do mathematicians not use real formal proofs?

Autism

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

Pretty much, except I can control it intuitively.

You have no idea what you are talking about

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.

>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.

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.

>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.

This.

What is it so hard to understand about this, it is like Veeky Forums never get this.

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

That is not the reason why people use high level languages

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

arxiv.org/pdf/1501.02155.pdf
Some do.

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

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.

>algorithmic complexity matters
Is what I said:

>coq is ready

We're writing maths, not logic.

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.

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

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

>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

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?

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

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

This just in: doing actual mathematics requires general intelligence.

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

Toplel. Please tell us more.

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.

>muh high emotional IQ

low iq brainlet found

>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.

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.