Hacker News new | ask | show | jobs
by wheresmycraisin 2152 days ago
Programming != proofs, or in general communicating abstract mathematical ideas. Writing mathematics is nothing like writing software.
2 comments

I don't think this is true (or at least not true for all programs); there's a whole discipline of software which shows how close writing software is to formal logic/inductive proofs in Agda Coq, etc.
What I am trying to convey is writing software is better than writing maths, just like medieval music notation vs modern notation. Programming is better than proving because most proofs are mere tautologies or artificial constraints. This is why theorem provers in code rely on term rewriting.

A triangle has a sum of 180 ? Well how about if you push the triangle inside out. In code you can easily run a more complex simulation which gives you all possible values of the sum ... which is why ascertaining useful facts like 180 ad-nausea is boring at best. In fact most mathematics if it can't be simulated can't exist.

Ok, then convince me. Write 'software' of, say, the proof of the the dominated convergence theorem or something else reasonably advanced and let's compare it to the proof in conventional math notation.
I'm guessing there was a physical intuition behind the theorem, if you can simulate it you will probably do something better than the proof. Now it's your turn to tell me why 1 + 1 = 2.
Honestly what are you talking about. You can simulate for 100 years without finding a counterexample, but that doesn't make a proof. The whole point of math is to understand why things are true, not to just be satisfied that it seems true.
The way I see it ... Most mathematicians nowadays use mathematica or matlab or even python, proving my point. The notation is medieval ... and probably the only reason it survives is because of form factors of paper.

> Mathematics is a part of physics. Physics is an experimental science, a part of natural science. Mathematics is the part of physics where experiments are cheap.

https://www.uni-muenster.de/Physik.TP/~munsteg/arnold.html

I see simulating as a part of the experiment. If the proof is wrong it wouldn't last a seconds worth of simulation. I suppose a proof in essence is a pattern or an invariant of the system ... but most proofs have really no meat to them. The notation is merely intimidating like obfuscated code.

> The way I see it ... Most mathematicians nowadays use mathematica or matlab or even python, proving my point.

Yes. But most of us don't use those to prove anything; rather, a lot of us use it to implement computations based on those proofs (and do some exploratory "could this possibly be tru?" kind of work). Useful tools, for sure, but not something that remotely proofs your point. Most mathematicians also eat bread. That does not mean that math is a baked good.

> The notation is medieval ...

It is not. Read Gauß or Euler from the 18th and 19th century, and the notation is nothing like modern mathematical notation. I can't even imagine what medieval mathematics notation looks like!

> https://www.uni-muenster.de/Physik.TP/~munsteg/arnold.html

That is indeed the opinion of Arnold, a giant of mathematics. An opinion that, I daresay, does not reflect the majority opinion on mathematics.

> I see simulating as a part of the experiment.

Sure. Simulating is a valuable experimental tool to many mathematicians (where available; of course it isn't always).

> If the proof is wrong it wouldn't last a seconds worth of simulation.

At face value this statement betrays how little you know about this matter. There can very well be errors in proofs that cannot be uncovered without thousands of years of simulation, if at all.

Now, even interpreting your statement in the best possible light, namely something along the light of "simulation can often uncover mistakes in proofs", I would say: fine, but what about the converse?

> but most proofs have really no meat to them. The notation is merely intimidating like obfuscated code.

Are you insane? Take something that is patently "useful" and patently "real world", like the fundamental theorem of calculus. Meatless?

"Mathematics is a part of physics."

It's kind of amazing how quickly that article got so wrong. Math isn't a subset of physics. Physics is the estranged brother of Math, always needing to borrow some money from him or else the power goes out or he can't afford food or some other sob story.

See Principia Mathematica, A. N. Whitehead and B. Russell, Proposition 110.643
1 + 1 = 10
> Now it's your turn to tell me why 1 + 1 = 2.

By construction.