Documenting mathematics rigorously is actually hard. For example see the Formal Abstracts (<a href="https://formalabstracts.github.io" rel="nofollow">https://formalabstracts.github.io</a>) project by Thomas Hales. Hales' other writings on the subject may be informative too: <a href="https://jiggerwit.wordpress.com/2019/06/20/an-argument-for-controlled-natural-languages-in-mathematics/" rel="nofollow">https://jiggerwit.wordpress.com/2019/06/20/an-argument-for-c...</a>
Hello, this is the creator of MathLingua.<p>MathLingua is still in development, and the documentation still needs work.<p>However, I wanted to get feedback earlier rather than later to help guide development and the writing of the docs.<p>Note that MathLingua is the language that powers <a href="https://mathlore.org" rel="nofollow">https://mathlore.org</a>.
This is an awesome effort!<p>Regarding a comment on possible use cases.. One component that would really compliment this would be a programming-language specific checker of definitions. In the documentation's example of "integer" it would be straight forward to write in python a function that checks if a given variable is an integer. The same can be for other definitions such as "invertible matrix" or "set of orthonormal vectors".. other languages could provide such checks for more symbolic stuff like "commutative ring" etc.<p>Once you have this in place, you can load your nice data into a (e.g.) numpy.ndarray object, and checks would be triggered for all possible properties. This would automatically tag your data as, e.g. "stochastic matrix" and then you could even get suggestions of the sort of "build a time-discrete stochastic system based on this matrix?". This is would be very helpful for "data scientists" who are a bit far from theory.. at least I know I would use this very often.<p>There is of course the issue of expressivity to be taken into account. Much of mathematical progress involves invention of new notation, not all of which is neatly written in "left to right English with only binary operators" (think of commutative diagrams for example). While the language can of course be expanded in this direction, there will be a very big temptation (and I would guess frequent pushes from the future community) to change to more and more general languages. In this case, please always keep in mind the very expressive but useless notation of Russell & Whiteheads's Principia. There is a big theory of language and expresivity, and there are also practical examples (think of OWL or other semantic-web languages) of how to reach a compromise that allows for enough expressivity for the use cases of interest.
Nice project! I'm working on something similar with <a href="http://fungrim.org/grim/" rel="nofollow">http://fungrim.org/grim/</a> and <a href="http://fungrim.org/" rel="nofollow">http://fungrim.org/</a>
A Google Group has been created to discuss MathLingua and Mathematical Knowledge Management at <a href="https://groups.google.com/d/forum/mathlingua-discuss" rel="nofollow">https://groups.google.com/d/forum/mathlingua-discuss</a>.<p>Everyone is welcome to join.
Would it be possible to put the theorem name (and possibly a description) at the top instead of buried at the bottom in a metadata block?<p>Theorem: “Fundamental Theorem of Calculus”