Hacker News Reader

The act of formalizing mathematics in a way that can be machine verifiable is an active area of research, but not one that is much of a concern to the majority of mathematicians. I will say that in the current state-of-the-art writing machine verifiable proofs is often quite difficult and unintuitive, and not possible yet for many branches of math. The foundations upon which generations of mathematics are based upon do not lend themselves to machine verifiable proofs. Placing these fields on such foundations is very non-trivial, but people are trying.

To your points on notation, I think requiring math to use purely ascii characters would end up being more of a burden than you expect. There are a lot of concepts in math and having more characters to use to represent them in a small space is helpful. I would much rather see a phi (one char) than a word representing something because it's easier to parse. Succinct notation lets you abstract big concepts and express relationships between them in a big-picture sort of way without requiring multiple lines. Then it's easier to remember the resulting relation.

It's also worth noting that a piece of notation generally doesn't have one global use throughout mathematics. As long as notation is defined it's generally not a problem.

Ever try to freestyle your own symbols while writing code? It doesn't go so well. There is extremely little freedom in the characters that you can code with. Coding is also rife with abstraction and complexity. All of the problems and barriers to learning that you describe exist with coding and are arguably worse. Yet, like mathematics, computer science is budding and creative; you just need to drudge through some busy work before you get to the edges of current knowledge.

Your remark about professors not knowing what they teach in some sense is mean-spirited.

If you don't like how mathematics is written or taught then just write something else and use different language. All you really need to do is communicate your logical point. With computers, on the other hand, you can't just write your own language or run any type of software on your hardware.

>Forget executability for now but even just having a convenient way of parsing a formula, havings its notation explained to you automatically.. that would be so important

>To me, math notation is a programming language...

That's the thing though - it's not. It's a language, but not a programming language. It's not strict. It's by humans, for humans.

Why is it so clunky sometimes? Because explaining things is not easy. People are trying their best, but in the end, they get together after the conference talks over a glass of beer and go "Well, here's what's really going on there".

Have you ever been in a state where you know what you want to say, but just can't find the right words for it? That's the perpetual state of mathematical writing.

>You probably agree that the vast majority of math papers are never read by more than two people, the original author and the reviewer.

Unlikely. Usually, there are groups of people who get together at conferences and talk about what they do. Mathematicians rarely work in isolation.

>Every paper could be like a programming library

In a way, they are -- but the hardware is your brain. You can't make the computer do the work for you -- no more than we could improve on this very comment. In the end, the paper is communicating ideas.

Yes, there's work on people formalizing math to turn proofs into computer programs. The result is machine-verifiable, but unreadable - as is often the case with code anyway; without documentation, it's not easy to understand what the code is doing.

>Then let's read the API docs to get which final formulas are usable to me now that you wrote this paper.

But math is not about formulas. Often it's about concepts, constructions, patterns, ways of looking at things.

>We need to find a way to write math more efficiently on the computer now so we can get better and faster at it

I don't think tooling is the bottleneck, really. We have LaTeX, which is easy enough to use, in my opinion.

---------------- That said, one person that would agree with you is Stephen Wolfram.

Mathematica Notebooks are pretty much exactly what you describe: they are executable papers, where you can mix text with computations and code, etc.

One reason they are not the norm is that Mathematica is a product that costs $$$ (although the engine is free with RaspberryPi, and Notebook reader is free, IIRC). They are going the way of the cloud now, though.

The competing FOSS solution is SAGE math: http://www.sagemath.org/ - but it's more of code-for-math than the concept you describe. Mathematica hits it on the nose.

It's been around for a while, but still didn't really catch on.

Part of it is proprietary format, part of it is inertia -- but part of it is that it's often not what the authors want.

What the authors want is tell a story, not create an executable object. The symbols are just crutches.

I think the real problem is that the story-telling aspect is thrown away in many papers, leaving the place only for the result. People don't like showing the dirty work, the unfruitful steps, their thinking that brought them there. The informal, gritty stuff. (They leave it for beers after the talks).

But that's not how it used to be. I was trying to learn about quaternions one day, and found the original lectures by Hamilton, their inventor. It read like a novel. That's how math writing should be. It degenerated in the last 100 years or so, but it's coming back to life now, I think.

>Whoever sits at these prestigious journals in my opinion is already being paid for this very job: to make sure that papers are accessible.

HAAHAHAHAHAHAHAH. HA. HA.

Sorry, my friend, let me ruin your world view here.

First, effectively, nobody sits in the journals. Mathematicians write papers, other mathematicians review them - voluntarily. The journals are often little more than matchmakers. That's why we are having a revolution of sorts now: people are starting to ask why we need the journals in the first place. And some people outright believe that we don't - that ArXiV (the website where mathematicians put their papers without review) is enough.

Secondly, nobody gets paid. Mathematicians don't get paid to write papers, reviewers don't get paid to review. There is an immense pressure to publish, but it's not like one gets paid per paper.

If you mean the publishers that host the papers - their purpose is to make money off subscriptions, and that's about it. #downwithelsevier

Why do people still try writing good papers? Because they want the ideas in those papers to spread. Why do papers still suck? Because explaining something clearly is hard.

>Also I don't think that a math notation which has symbols that don't even exist on ascii keyboards should be acceptable.

And everyone should just speak English. Увы, увы, было бы довольно печально жить в таком мире.

>I will read your link.

Please please please come back here and share your thoughts when you do! Can't wait to hear them.