Lint for Math
rjlipton.wordpress.com
rjlipton.wordpress.com
As with programming languages, the first question is what each variable is, and what its type and definition are. You should be able to mouse over variables in textbooks and see that information. You should be able to see formulas fully parenthesized if you want. (The machine learning people are terrible about inventing new operators and not telling the reader what their precedence is.)
Mathematica notebooks come close to this. But books and papers on math are not usually published that way. MathML was a step in the right direction but didn't catch on.
If you want to seriously address this issue, you need to make sure it works for the mathematicians who work at the most abstract levels of the hierarchy. Mathematics as a language is primarily about communicating an idea from one human to another. The problem here is that pure mathematicians want and need to bend type rules for the sake of communication. There are implicit equivalences of types all over the place. For example, a homotopy is a smooth map (between more than one kind of space depending on your preference), but it is also a statement of equality between two things, and it is a commutative diagram involving infinite sequences of objects and operators which is defined in contexts where smooth maps do not exist. Whether or not these different things can be used in the same place depends not on the type of the definition but the greater context of the paper.
Moreover, not all variables have definitions you can annotate. Sometimes the definitions are assumed to exist for the sake of contradiction, sometimes they are the unique limit of some crazy sequence that takes a page to write down. Sometimes they are defined by properties they have, so they don't represent a single object but a family of objects (or maybe it is a single object, who knows?)
I'm not saying better math documents are impossible. I'm saying that most programmers who claim that we need a better way to do it don't appreciate the depth and complexity of the problem.
I think probably a better solution is to augment a public repository of papers (such as arXiv) by allowing readers to add inline annotations explaining concepts, fixing bugs, etc. The real tragedy is that once a person figures out what the hell is going on in a poorly written paper, they have no way to bring their insight to anyone reading the same document in the same place.
I agree with you times infinity.
I get frustrated when programmers are used to looking at source code that has very precise meaning and are expecting to be able to read mathematics as if it were source code too. Or worse, when people think that the hardest part of understanding mathematics is the notation. Or that a capital sigma means a sum in all contexts, or that a lowercase sigma could not possibly mean anything other than a standard deviation or a lowercase pi could not mean anything other than the first positive root of the sine function.
Mathematics is written by humans for humans. Trying to automate mathematical writing or reading is about as feasible as trying to automate literary analysis of 19th century romanticism[1]. Or in Weierstrass's words to Kovalevskaya,
[...] it is true that a mathematician who is not somewhat of a
poet, will never be a perfect mathematician.
[1] When reading Riemann, I particularly feel like I might as well be reading E. T. A. Hoffman sometimes. Some of the moves he makes I cannot describe as anything but poetical. For example, how he describes the contours of integration in a couple of reformulations of the zeta function.
Sure. But since I can't directly probe your mind, I can either read through thousands of pages of manuscript to refine my internal mental model of the particular theory/problem set/subfield, or hope for an interactive system that allows me to do just that, where I can tinker with concepts and connections between them.
Bret Victor showed it best, and even though he was talking about the applied side, it goes perfectly for the more abstract areas too.
This is where Bret Victor and I disagree: interactive documents for visualizing circuit diagrams do not generalize perfectly to all of mathematics. If you want to develop a generic tool that allows any mathematician to build interactive documents for tinkering with concepts, you need to see how deep the mathematical rabbit hole goes. Victor's tools are a proof of concept for very limited systems.
Because to effectively understand a concept (usually through applications of it either in full blown proofs, or in smaller calculations - that are just ad-hoc proofs) you need the right level of verbosity. Oversaturation with low-level set theory steps from Burbaki won't make anyone understand systems of differential equations, but when you are unsure of a step, you need a bit more detail.
And in my experience the optimal trajectory through a proof is almost always different for everyone. So it'd be good if proofs were "discoverable", expand and collapse steps.
And we don't even have to go crazy with "reverse mathematics"-like axiom chasing. But the current practice of throwing random symbols on pages in LaTeX is rather suboptimal in my opinion.
I'm not sure that any plaintext markup can be sufficiently compact, semantic, and still resemble the handwritten syntax. That means we'll probably have to come up with a more interactive input method that is a bit more WYSIWYG in nature and has some auto-complete and automatic parenthesizing.
If we trigger an error for ambiguous cases, the path of least resistance is to make things unambiguous.
Tools like mathematica and MS equation editor have solved this at the same time as the input method question: have an input method which converts to a markup in the background. This markup has enough information to produce typeset output.
is to parse this way:
4 + –1 * –2–1 ^2
This is a LISP expression:
(LIST 'PLUS (DIFF (CADR EXPR) X) (CADDR EXPR) X))
LIST 'PLUS DIFF CADR EXPR X CADDR EXPR X)
Likewise font size, exact character placement vertically, visual cues, color (more deeply nested = redshift) can all make it super-easy to instantly parse things.
Instead the computer gets it instantly (super-easy to parse nested parantheses for the computer) but doesn't convey that to us at a glance at all.
And as much as I value good, clean code and style guides in programming, the TeX source of formulas are never read and usually edited by a single person, even in large collaborative projects.
And yet I wasted lots of time trying to make sense of papers containing such errors. So I would appreciate such a tool.
However, when, as a graduate student, one encounters the task of
reading a technical mathematical paper for the first time, it is
often the case that one loses much of one's higher reading skills,
reverting instead to a more formal and tedious line-by-line
interpretation of the text. As a consequence, a single typo or
undefined term in the paper can cause one's comprehension of the
paper to grind to a complete halt, in much the same way that it
would to a computer.
There's more context here:
https://terrytao.wordpress.com/career-advice/there%E2%80%99s...
In addition, much of the math out there is described in words, rather than pure formulae. Humans are capable to reason about these things because we are trained to have an abstract understanding of what these things mean in a given context (and we can actually understand text).
A naive implementation of checking correctness of equations would likely return an incomprehensibly long list of cases where your equation might not make sense. A program that could check each and every step of your computation needs to understand your notation and definitions. While this is possible in principle – I assume you could do that for one particular problem with Mathematica – it would take you at least a few orders of magnitude more time to implement your sanity-check program for a particular problem than to check your equations by hand.
That's not to say this line of reasoning is not worthwhile. PLT Redex already does something similar for programming language semantics: http://redex.racket-lang.org/. Catching bugs in programming language semantics works for the same reason catching bugs in C works. There is a formal grammar with well-defined meaning that doesn't exist in general mathematical discourse. There is work being done in that direction as well: http://homotopytypetheory.org/book/. I wouldn't call that linting though.
They make a huge difference if the reader wants to reuse a certain formula without deriving everything in sight. The time necessary to use a formula is no longer O(1), but O(n) with n being the length of the preceding discussion.
It also means you can't look at two expression and immediately check if they are equivalent as the variables might have different semantics.
Plus, you don't get to correct the mistake in the original, so every time you (or someone else) have to read it, you might need to redo the calculations just to be sure.
As for correcting mistakes I usually go to the author's homepage to find the most up to date versions along with errata. These days most papers are put up on the arxiv anyway which is often more up to date than whatever is printed in a journal so fixes for minor errors is again a non-issue.
Before catching errors, I think an easier target for a tool like this would be to enforce notation, e.g. permutations are always called π not σ, and vectors are always \vec{v} not \mathbf{v}. This would be useful for multi-author texts like wikipedia.
I would recommend a compiler which translates a subset of a clean math notation (which could be identical to the math subset of LaTeX) to native LaTeX, which includes a lint algorithm, and which also supports special graphics packages (PGF/TikZ for instance).
This approach would keep the compiler small and maintainable while retaining 100% compatibility with LaTeX.
On the other hand, most of mathematics can be done in first order logic (FOL).
As for English, I'm not much of a linguist but I believe the closest equivalent to the above for English (and other natural languages) would be Categorical Grammar or maybe Montague grammar.