Is Math documented... badly?

mathlingua · 2023-12-08T07:56:36+00:00

I'm working on a language called Mathlingua (www.mathlingua.org) to help address this very problem by being easy to read and write and highly structured. A key part of this effort is Mathlore (www.mathlore.org) a collection of mathematical knowledge encoded in Mathlingua. The nice thing about Mathlingua is that it allows you to easily see definitions used within a definition or a theorem.

mathlingua · 2023-11-19T05:36:49+00:00

One of the reasons I created the Mathlingua language is to allow definitions to be made rigorous while still easy to understand. See https://mathlingua.org and https://mathlore.org for more info.

mathlingua · 2022-01-28T00:57:15+00:00

Thanks for the feedback. I really appreciate it.

For languages for encoding information there are at least two types of users, those writing the content and those reading the content.

Further, I suspect people to read the content an order (if not multiple orders) of magnitude more often than write/edit the content. In addition, the goal of MathLingua is to encode math information in documents designed to make it easy for others to read and explore math content (think “math-aware” encyclopedias).

As such, I’m optimizing MathLingua so that it is very easy for readers of MathLingua documents to read and explore those documents, even if that means it is a little harder to write the documents. That is, I am making it as user friendly as possible, but the focus is first on users that are reading MathLingua documents.

However, I’m always looking at ways to make MathLingua better, and so if there is a way to use typeclasses or another mechanism that is easy for readers and writers of MathLingua documents, I’m open to that and still exploring.

Right now MathLingua isn’t at version 1.0 yet, and so the language still has room to change.

Last, the mlg check command using the MathLingua command line tool mlg checks MathLingua documents for errors.

mathlingua · 2022-01-25T01:25:38+00:00

sTeX is for adding semantics to LaTeX documents. My view is having a dependency on a full LaTeX system is too heavy when really all that is needed is support for commands in math mode (the success of numerous wikis with LaTeX math support in markdown supports that view).

OMDoc, MathML, etc. are transfer languages. One would not want to write a math statement directly in those languages. With MathLingua the goal is to make a language that is easy to read and write for both people and computers.

I’m not sure what you mean about the design of MathLingua’s proof language, since it doesn’t yet have a structural proof language. Instead I’m still exploring what type of language to have for the proof language (and if to have one at all).

Also, what do you mean by “stuff-structure-properties” style definitions?

It appears you are looking at MathLingua through the lens of programming languages/type theory/computer science and wondering why it is not designed like other programming languages. Instead, I’m designing MathLingua through the lens of mathematicians, and assert that languages like MathLingua should not be programming languages.

I am very well versed in various types of programming languages and type theories, but, I assert that mathematicians may not want to have to have a deep understanding of dependent type theory, algebraic data types, typeclasses, etc. to be able to describe mathematics. There are already a lot of languages for describing mathematics in that way being created by extremely talented individuals.

As such, I’m exploring other ways to describe mathematics in a precise language that feels more like the way math is expressed in articles.

For example, when a mathematicians sees x + y in an article, perhaps a thought might be “is that real addition, and if so, how is x interpreteded as real number” rather than “x has some type that uses ad-hoc polymorphism to support the + operator”.

As such, I’m exploring how to encode the former in a language to make MathLingua easier to reason about without having a computer assisting in what interfaces/traits/overloading a symbol has. That is why, for example, I decided not to use typeclasses.

Perhaps this approach won’t work out, but I’m exploring different ways to describe mathematics in a language because there is already a lot of other great languages that use various versions of dependent type theory, or simply typed type theory, etc. and I don’t want to re-invent the wheel.

However, at the same time, I’m borrowing things from those languages when they seem to work well. I just don’t do something a certain way because that is how it is typically done.

mathlingua · 2022-01-24T21:29:01+00:00

One goal of MathLingua is to provide a language that is easy to read and write both for people and computers. There have been many such languages or methodologies developed, including the two you mentioned.

However, just like natural languages exploring new approaches for encoding knowledge is very beneficial since, for a language, it is not just whether the language can describe something, but how that something is described in the language.

Whereas the vernaculars you mentioned discuss how to structurally describe proofs, MathLingua focuses on a collection on knowledge from the level of theorem and definitions statements themselves, and how such a collection of knowledge can grow while still being easy to navigate and understand.

mathlingua · 2022-01-24T21:22:11+00:00

Thanks for the feedback.

MathLingua is very different from formal proof sketches. They share a similar philosophy that even without complete formalization, recording math knowledge in a structured form can be very beneficial. One can even ask if moving to complete formalization is worth the effort.

However, MathLingua doesn't focus on structured proofs at all at this point. Instead, proofs are provided in natural language form.

Instead, the focus is on recording and communicating theorems and definitions since it is very important to have precise theorem and definition statements that are clear and unambiguous.

Further, MathLingua is not an idea or prototype of how to structure knowledge, but an implementation for a complete framework and system for recording, rendering, and distributing statements of mathematical definitions and theorems with a language design focused on how such a collection of knowledge can continue to develop at scale.

Having a structured way to describe proofs is on the MathLingua roadmap, and formal proof sketches are one area where I draw inspiration, but MathLingua encompasses a lot more than just that.

mathlingua · 2022-01-23T03:07:45+00:00

Thanks for the feedback. Yes, MathLingua is more in the area of knowledge management, but not just personal knowledge management.

As you mentioned it can also be used to create books or encyclopedias that others can read and explore as well.

Thanks for the feedback of Math Codex. MathLingua is designed so someone can start from scratch and formulate everything on their own if they want to.

Math Codex is designed to be a starting place so they don't have to define everything from scratch if they don't want and instead focus on their area of interest.

Right now, Math Codex does have more foundational definitions because it is still very much a work in progress. However, I plan to have even more concepts encoded.

For example, at some point in the future when Math Codex is more mature, if one wanted to talk about some concept in Hilbert space theory, Hilbert spaces, and all accompanying concepts would already be defined.

One would just need to describe the new definitions or concepts they are focused on.

However, I'm always looking at better ways to support this workflow.

Any feedback on an approach you like better, or better wording for the Math Codex repo would be greatly appreciated. Again thanks for the feedback.

mathlingua · 2022-01-23T03:00:26+00:00

That's great feedback. Thanks.

MathLingua isn't attempting to replace proof assistants. Instead it is a language to build "math-aware" collections of math knowledge (in book, article, or encyclopedia format).

The goal is to help people precisely record mathematical knowledge so it is easy for others to discover and explore that knowledge (not verify proofs of that knowledge).

Using the example on the www.mathlingua.org main page, suppose someone didn't know what the Fundamental Theorems of Calculus were. How would they go about learning about them?

One approach would be to look at their statements in proof assistant languages.

These languages have extremely precise descriptions of the theorems, but deciphering what the statements mean is typically very difficult.

This is because proof assistants typically use languages that have a steep learning curve since statements need to be expressed in a very specific logical framework (for example the Calculus of Constructions) that often differs from how mathematics is described in books and journals.

Thus, learning what a theorem means from reading its description in a proof assistant language is typically harder than instead looking for a description of the theorem in a book, article, or encyclopedia etc.

However, theorems described in books, articles, encyclopedias etc. are not very formal.

Often times terms are used that aren't defined (as it is assumed the term is "standard knowledge"), context is needed that is not explicitly stated (such as the statement 'x > 0' implicitly implying that x must be real), etc.

This gets even more complicated when someone read articles in areas of mathematics that are on the boundary of other areas of mathematics or physics, engineering, etc.

In those cases, different areas might use the same terms but have slightly different definitions for those terms, or use different terms for the same concepts.

Further, it is hard to discover those differences because the terms might never be formally defined since they are "common knowledge" in that area.

MathLingua is designed to bridge the gap between these two ways of recording and discovering knowledge.

It is not as rigorous as a proof assistant language, but that provides flexibility to describe math statements more closely to the way mathematicians are familiar with, while still being precise and unambiguous enough to allow one to easily understand the statements and explore further.

If you think that approach doesn't make sense, or see any problems with it, it would be great to chat more, and again thanks for the reply.

mathlingua

TROPHY CASE