6 ms·

Lint for Math

dkarapetyan 12y ago
In the grand scheme of things all the errors he mentioned do not make a difference to the overall direction of the proof. Syntactic errors in programs on the other hand do. Unused variables, equality instead of assignment, declared but uninitialized variables, etc. are almost always bugs. That's not the case with math. 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/ 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/ http://homotopytypetheory.org/book/. I wouldn't call that linting though.
- conistonwater 12y ago
  > In the grand scheme of things all the errors he mentioned do not make a difference to the overall direction of the proof. 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.
  - dkarapetyan 12y ago
    Then you and I are talking about different things. I don't read a mathematical proof to see what formulas I can copy. I read a mathematical proof to re-use the techniques in some other domain and to understand it I have to follow along and re-create bits and pieces of the proof. Obvious mistakes like the one mentioned in the post do not hinder that process. Less obvious errors would not be caught by a linter. 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.
    - conistonwater 12y ago
      I'm not talking about "reading a proof to see what I can copy", it's about being able to rely on what is written there. Also, there are many papers that serve as references that I want to be able to look up quickly. Rederiving every result any time I want to use it is not the way to go.
  - EpicEng 12y ago
    So... Kind of like the risk you take when you copy and paste code without first attempting to understanding it? I can't say that I've ever read through a proof just to nab a formula without even thinking through the material.
Animats 12y ago
We really need a better way to represent math in documents. TeX/LaTex is all about putting ink on paper in a pretty way; it doesn't know anything about the math. 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.
- wtallis 12y ago
  The problem is that there are actually several components needed: the semantic markup language, an input method no less efficient than LaTeX, and the math-lint itself. LaTeX is not semantic. MathML is just too verbose to type in the raw. The syntax used by theorem-proving software tends to be both esoteric and a bit too verbose (in addition to requiring the statements themselves to be extremely verbose). 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.
  - kibibu 12y ago
    One of the reasons is surely that different fields of maths/engineering reuse the same symbols to have different meanings.
    - chriswarbo 12y ago
      We know how to do type-directed operator overloading in unambiguous cases, eg. static methods in OO, modules and typeclasses in FP. This is often (ab)used to distinguish between alternative definitions. For example, Haskell's Monoid module defines several type synonyms for booleans and numbers, each of which has a different Monoid definition: https://hackage.haskell.org/package/base-4.7.0.2/docs/Data-Monoid.html https://hackage.haskell.org/package/base-4.7.0.2/docs/Data-M... If we trigger an error for ambiguous cases, the path of least resistance is to make things unambiguous.
vortico 12y ago
Simple errors like these cover maybe 0.01% of the issues in a common math paper draft. Scrutinizing human review is required to catch "intellectual errors" such as introducing a concept before the reader is mentally prepared for it, or by offering an explanation in too much or little depth. During review, typographical errors (e.g. $10^12$) and "type-checking" errors (e.g. "r ∈ R vs. r ⊆ R") should be obvious to reviewers, so I feel it would be an extremely low priority to develop and apply a tool to fix these trivial issues. 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.
- perlgeek 12y ago
  > Simple errors like these cover maybe 0.01% of the issues in a common math paper draft. And yet I wasted lots of time trying to make sense of papers containing such errors. So I would appreciate such a tool.
  - jordigh 12y ago
    Terry Tao has a blog post about these "compilation errors": 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. https://plus.google.com/+TerenceTao27/posts/TGjjJPUdJjk https://plus.google.com/+TerenceTao27/posts/TGjjJPUdJjk There's more context here: https://terrytao.wordpress.com/career-advice/there%E2%80%99s-more-to-mathematics-than-rigour-and-proofs/ https://terrytao.wordpress.com/career-advice/there%E2%80%99s...
ivan_ah 12y ago
Cool idea. Parsing LaTeX into an AST with awareness of math structure (e.g. taking into account symbolic transformations like x^{1/2}=\sqrt{2}) would be a good start. 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.
- progman 12y ago
  Parsing LaTeX would be a heavy task due to LaTeX's innumerable packages. 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.
unknownian 12y ago
Is there a word to describe the structure of the notation of mathematics versus programming syntax versus the English language?
- swatow 12y ago
  Most of programming is done in something reminiscent of type theory. Actual languages are more complicated because they either are impure (C, C++ etc) or involve non-total functions (Haskell). Idris, Coq and Agda can be reduced to some sort of type theory. 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.
UnitaryOperator 12y ago
TEst
wz1000 12y ago
Coq[0] provides functionality that is an extension of this concept. It checks your proofs for you! [0]- https://coq.inria.fr/ https://coq.inria.fr/
QuantumRoar 12y ago
I don't think this is going to be possible until computers are smart enough to understand high level maths (theorem provers have still a long way to go). A hundred different fields of research have a hundred different notations which are usually assumed to be convention and the reader is expected to know about these. The i in the summation could also refer to the imaginary unit but only if you are talking to physicists/mathematicians. Engineers use a j instead. Or what about conventions such as Einstein summation or infix operators defined by a set of axioms? How do you even recognize what a variable is or that \oplus is likely an operator or that z^*z is not a typo but a superscript indicating complex conjugation followed by an implicit multiplication symbol? 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.

In the grand scheme of things all the errors he mentioned do not make a difference to the overall direction of the proof. Syntactic errors in programs on the other hand do. Unused variables, equality instead of assignment, declared but uninitialized variables, etc. are almost always bugs. That's not the case with math. 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/ 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/ http://homotopytypetheory.org/book/. I wouldn't call that linting though.

conistonwater 12y ago
> In the grand scheme of things all the errors he mentioned do not make a difference to the overall direction of the proof. 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.
- dkarapetyan 12y ago
  Then you and I are talking about different things. I don't read a mathematical proof to see what formulas I can copy. I read a mathematical proof to re-use the techniques in some other domain and to understand it I have to follow along and re-create bits and pieces of the proof. Obvious mistakes like the one mentioned in the post do not hinder that process. Less obvious errors would not be caught by a linter. 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.
  - conistonwater 12y ago
    I'm not talking about "reading a proof to see what I can copy", it's about being able to rely on what is written there. Also, there are many papers that serve as references that I want to be able to look up quickly. Rederiving every result any time I want to use it is not the way to go.
- EpicEng 12y ago
  So... Kind of like the risk you take when you copy and paste code without first attempting to understanding it? I can't say that I've ever read through a proof just to nab a formula without even thinking through the material.

Animats 12y ago

We really need a better way to represent math in documents. TeX/LaTex is all about putting ink on paper in a pretty way; it doesn't know anything about the math. 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.

wtallis 12y ago
The problem is that there are actually several components needed: the semantic markup language, an input method no less efficient than LaTeX, and the math-lint itself. LaTeX is not semantic. MathML is just too verbose to type in the raw. The syntax used by theorem-proving software tends to be both esoteric and a bit too verbose (in addition to requiring the statements themselves to be extremely verbose). 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.
- kibibu 12y ago
  One of the reasons is surely that different fields of maths/engineering reuse the same symbols to have different meanings.
  - chriswarbo 12y ago
    We know how to do type-directed operator overloading in unambiguous cases, eg. static methods in OO, modules and typeclasses in FP. This is often (ab)used to distinguish between alternative definitions. For example, Haskell's Monoid module defines several type synonyms for booleans and numbers, each of which has a different Monoid definition: https://hackage.haskell.org/package/base-4.7.0.2/docs/Data-Monoid.html https://hackage.haskell.org/package/base-4.7.0.2/docs/Data-M... If we trigger an error for ambiguous cases, the path of least resistance is to make things unambiguous.

vortico 12y ago

Simple errors like these cover maybe 0.01% of the issues in a common math paper draft. Scrutinizing human review is required to catch "intellectual errors" such as introducing a concept before the reader is mentally prepared for it, or by offering an explanation in too much or little depth. During review, typographical errors (e.g. $10^12$) and "type-checking" errors (e.g. "r ∈ R vs. r ⊆ R") should be obvious to reviewers, so I feel it would be an extremely low priority to develop and apply a tool to fix these trivial issues. 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.

perlgeek 12y ago
> Simple errors like these cover maybe 0.01% of the issues in a common math paper draft. And yet I wasted lots of time trying to make sense of papers containing such errors. So I would appreciate such a tool.
- jordigh 12y ago
  Terry Tao has a blog post about these "compilation errors": 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. https://plus.google.com/+TerenceTao27/posts/TGjjJPUdJjk https://plus.google.com/+TerenceTao27/posts/TGjjJPUdJjk There's more context here: https://terrytao.wordpress.com/career-advice/there%E2%80%99s-more-to-mathematics-than-rigour-and-proofs/ https://terrytao.wordpress.com/career-advice/there%E2%80%99s...

ivan_ah 12y ago

Cool idea. Parsing LaTeX into an AST with awareness of math structure (e.g. taking into account symbolic transformations like x^{1/2}=\sqrt{2}) would be a good start. 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.

progman 12y ago
Parsing LaTeX would be a heavy task due to LaTeX's innumerable packages. 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.

unknownian 12y ago

Is there a word to describe the structure of the notation of mathematics versus programming syntax versus the English language?

swatow 12y ago
Most of programming is done in something reminiscent of type theory. Actual languages are more complicated because they either are impure (C, C++ etc) or involve non-total functions (Haskell). Idris, Coq and Agda can be reduced to some sort of type theory. 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.

UnitaryOperator 12y ago

TEst

wz1000 12y ago

Coq[0] provides functionality that is an extension of this concept. It checks your proofs for you! [0]- https://coq.inria.fr/ https://coq.inria.fr/

QuantumRoar 12y ago

I don't think this is going to be possible until computers are smart enough to understand high level maths (theorem provers have still a long way to go). A hundred different fields of research have a hundred different notations which are usually assumed to be convention and the reader is expected to know about these. The i in the summation could also refer to the imaginary unit but only if you are talking to physicists/mathematicians. Engineers use a j instead. Or what about conventions such as Einstein summation or infix operators defined by a set of axioms? How do you even recognize what a variable is or that \oplus is likely an operator or that z^*z is not a typo but a superscript indicating complex conjugation followed by an implicit multiplication symbol? 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.