HN user

CatsAreCool

199 karma
Posts6
Comments49
View on HN

I'm working on a language MathLingua (www.mathlingua.org) whose goal is to precisely describe mathematics using a format that is easy to read and understand to help address ambiguity in mathematical texts written using natural language.

It is still a work in progress, but does it help address some of the problems you see in learning mathematics? Any feedback is greatly appreciated. Thanks.

It is similar. However, where omdoc seems to focus on storing math concepts in a precise way, it’s focus doesn’t appear to be on easily hand writing concepts in that format.

MathLingua, on the other hand, focuses on being precise and easy to read and write in its raw form.

Great feedback. This is one of the areas that I designed MathLingua to help with.

Every definition has a ‘written:’ section describing how to express the math idea on paper and a ‘called:’ section describing how it is described when speaking.

Right now the ‘written:’ is used to render how a result looks, and in a similar way the ‘called:’ section can be used to convert a result into a transcript that a screen reader would read.

I haven’t yet been able to implement this feature though, but stay tuned for updates.

Yes, you can. MathLingua makes no assumptions about what symbols are used to represent different math operations (other than KaTeX is used to render expressions and so you need to symbols KaTeX recognizes).

As such you can use whatever visual representation you want for operations and definitions.

For a particular math definition, you can also specify multiple different notations for the concept (in this case, MathLingua uses the first one when rendering results).

An example of this is the derivative of a function in the “A Detailed Example” section of the docs.

This is the creator of MathLingua, a unique language for easily describing mathematical definitions, theorems, axioms, and conjectures.

It is unique from LaTeX and theorem proving languages and has a different goal. See the documentation at www.mathlingua.org for more information.

This post is a follow-up to https://news.ycombinator.com/item?id=23960662 and many changes have been made to MathLingua since that time based on the feedback from that post.

In particular, since that time, I have added numerous improvements to the language to improve its usability, have drilled down on a particular use-case that I have documented more clearly, and have created a `mlg` command line tool to interact with the MathLingua language.

In particular, using `mlg check` one can check their MathLingua documents for errors, with `mlg document` one can create a dynamic static site of their documents suitable to be shared on GitHub pages, and with `mlg edit`, an in-browser IDE is available to edit your MathLingua documents with live previews, auto-complete, etc.

I really appreciate all of the feedback I received previously, and any and all feedback now is greatly appreciated.

I think having a tool but not being able to know how it works can be both amazing and frustrating at the same time (depending on the perspective of someone using the tool vs someone wanting to make the tool better).

Both perspectives are equally valid.

As a concrete example, suppose an alien cube suddenly appeared on Earth that, with a push of a button, would emit a pill.

It was discovered that the pill could cure half (but only half) of all known forms of cancer.

However, no matter how hard anyone tried, it was impossible to understand how the cube or the pill it created worked.

For those with cancer that took the pill and were cured, the cube was an amazing magical device.

For the people that took the pill and it didn't help them, the cube was worthless, since doctors couldn't tell them anything about why it didn't work, or what they could do to make it work.

For researchers it was frustrating because the cube showed some cancers are curable, but gave no reason why.

For the cancers it did cure, they didn't know why, and for those it didn't cure they also didn't know why.

Further it gave no insight into why only half were curable.

Was it because the cube was imperfect, or was that really the best that could be achieved?

For all intents and purposes, cancer research and treatment didn't really change. If you had cancer, you tried the magic pill. If it worked great. If it didn't, then doctor's were back to traditional techniques.

Thus from a knowledge perspective of one day curing all cancer, the cube didn't help, because the knowledge of how it worked couldn't be expanded to cure all cancer.

For someone cured by the cube, it was an amazing device, and nothing could change their mind.

For a cancer researcher, the cube was useless, and the only thing that could change their mind was if its mechanisms could be understood.

It is similar for math. As a tool, it is good enough to just know that the theorem is valid.

However, if you want to expand on that tool, develop more tools, or create different ways of looking at the problem, you need to understand why the theorem is true.

I thought of this, but couldn't find a nice way to fit this into the syntax.

That is,

  Theorem: "some text"
is the same as
  Theorem:
  . "some text"
Thus it would be hard to distinguish a named theorem with one statement
  Theorem:
  . "some name"
  . "statement 1"
from an un-named statement with two statements:
  Theorem:
  . "statement1"
  . "statement2"
So for now I'm leaving the name in the metadata section, but I'm open to putting the title higher if I can come up with a nice way to do so.

Thanks for letting me know about the typo.

The dot space is used to mark arguments since some arguments span multiple lines but are connected. For example, in

  Theorem:
  . for: x
    where: y
    then: z
  . 'some statement'
the 'for:where:then' group together is one argument, while the 'some statement' item is the second argument. The dot is needed to distinguish from
  Theorem:
    for: x
    where: y
    then: z
    'some statement'
where it is hard to tell where one argument stops and another starts.

It looks like there is a lot of shared interest in this area.

fspeech, fdej, and others, what do you think of having a Google group, mailing list, or something similar to have a communication channel for anyone that wants to chat more?

If you are open to this (or have another suggestion) I’ll set one up and share the link here.

If you prefer email, that’s cool too.

Your work looks really cool and your paper was a great read.

I too didn’t like the syntax of MathML, and I agree the semantics needs to be in the software.

For MathLingua I built a pattern matcher that is built in, but I haven’t tied MathLingua to a verifier.

I viewed these as separate things. This is because one can encode a statement but have a proof as a separate entity (which may be in a paper, digital, or verified form).

This allows one in mathlingua to express theorems and definitions from a book, for example, with references to the proofs in the book even though the results are not formally proven.

A layer on top of MathLingua would use MathLingua to formally verify statements. If this is needed, my plan is to leverage existing theorem provers for this.

Feel free to reach out by email if you want to chat more, or we can chat here. My email is on my github page https://github.com/DominicKramer.

I have a PhD in mathematics, I am a software engineer working at Google, and have practical experience with programming language design and usage.

MathLingua is not a Google product and is not affiliated with Google in any way. Instead it is my own work I am exploring at the intersection of math, computer science, language design, and natural language processing.

It would be great to chat more over email. My email can be found on my github page https://github.com/DominicKramer. Let me know if you have problems getting it.

Thanks for the feedback. I'll update the docs to make this more clear.

The goal is to allow the building of a system so someone could ask, for example, "what are the known theorems that describe when a function uniformly continuous?" or "under what conditions is a group solvable?".

To enable this, it is necessary to build a system that catalogs precise statements of math theorems, definitions, and other statements (https://mathlore.org is the start of this system that uses MathLingua but currently only uses keywords and some structure for searching).

This is similar to https://mathworld.wolfram.com or the math pages in Wikipedia except the statements are not text or LaTeX, that is hard for a computer to understand the meaning of. Instead the MathLingua language is used to identify math statements by meaning.

Right now the tooling can render math statements, find duplicate definitions, and can find missing definitions. Further https://mathlore.org uses MathLingua and has some basic searching.

Further, experimental work is also underway so that the MathLingua tooling can expand a math statement by expanding the definition of items used in that statement.

Yeah, I thought about using something like "A Language for Mathematics" but I thought "The Language of Mathematics" might draw more attention :) But it is only the title of my post on hacker news, not the title of the MathLingua website.

Thanks for the question. I thought about using LaTeX, however, it doesn't explain what a math statement means. Instead, it describes that it looks like. With MathLingua, the meaning is made precise so that a computer can understand the statement. (I'll make this more clear in the docs).

TLDR: Having a computer understand what a statement written in LaTeX means is a very difficult Machine Learning (Natural Language Processing) problem (if not impossible since math statements often have lots of hidden context).

For more details:

In LaTeX, what does "if $f$ is continuous on $[a, b]$, $f \geq 0$ there, and $\int_a^b f = 0$ then $f = 0$?

It looks clear at first, but what type of thing is $f$. From context of reading analysis books, it could be clear that $f$ must be a function because "continuous" describes functions (but can also describe other things).

Next, what does $\int_a^b f = 0$ mean? It is the integral of $f$ from $a$ to $b$, but is it the Riemann integral, the Lebesgue integral, the Darboux integral? Does the difference matter?

What exactly does $f = 0$ mean. Does it mean $f$ as a function is the same as $0$ as a function, or does it mean $f(x) = 0$ for all $x$? Are those two the same or different? Does the distinction matter?

All of these questions, show up after a computer has correctly parsed the sentence and identified the structure. However, just that step itself is a very hard natural language processing problem.

In fact, if someone comfortable in reading math was given a random theorem from a random paper and was told to explain what it means, they would likely have problems and would need to look at the context of the paper (or reference other papers) to understand the syntax. This just gives a feel for the difficultly to build a machine learning model.

That is why I decided to build a custom language. In MathLingua, for example, the theorem could be described as:

  Theorem:
  . for: f(x), a, b
    where:
    . 'a, b is \real'
    . 'a \leq b'
    . 'f is \continuous.function:on{\closed.interval{a, b}}'
    . 'f is \nonnegative.function:on{\closed.interval{a, b}}'
    . '\riemann.integral_a^b[x]{f(x)} = 0'
    then:
    . 'f is \identically.zero.function:on{\closed.interval{a, b}}'
It is more verbose, but gives a more precise meaning of what each item means. Then definitions can be made to describe what each referenced math definition means with a description of how its associated notation is written to make the rendering look similar to how it is written on paper.

For example, one could have the definition:

  [\identically.zero.function:on{A}]
  Defines: f(x)
  assuming: 'A is \set'
  means:
  . for: a
    where: 'a \in A'
    then: 'f(a) = 0'
  Metadata:
  . written: "f? = 0 \textrm{ on } A?"
This makes the definition more clear and the statement `g is \identically.zero.function:on{X}`, for example, is rendered as the familiar $g = 0 \textrm{ on } X$.

Other definitions can be written too, to make everything clear (or left for later. MathLingua doesn't require you to define the entire math universe before defining a more complex concept).

My response was a little long, but that is because there are a lot of subtleties that show up when trying to get LaTeX to work for describe the meaning of math statements. I hope this helps.

It is already difficult to have a formalized math language with a level of formality that matches that found in papers.

The goal of MathLingua, at this time, is to match such a level of formality that is in math books and papers.

However, the syntax was designed to allow support for transpiling to a theorem proving language to be added at a later time. It is something, in the future, that I would like to do, if possible, but I don't have a time estimate if/when it will be available.

Thanks for the links. I was not aware of Thomas Hale's research even though I searched extensively to try to find related work.

His descriptions of what he wants to attain align with what I would like, a formalized way to describe what is known in mathematics.

He also describes how this can be used for machine learning, and area that I am also pursuing, but my results are still in an exploratory state.

Either way, I am really glad others are looking into this area too. I think it is something that will be very beneficial to the math community.

I liked this article since it points out a problem in math where it can be hard to know what is currently known.

Perhaps a result can be proven using a little known proposition in a completely different area of math, but it is hard to find that result in the literature.

That is one reason I came up with https://mathlore.org. It is a place to collect mathematical info (with links to articles for a deeper look) so you or others can find it later when you need it.

It supports of public collection of math info as well as allowing you to build your own private collection so you can keep track of what you have learned.

The hope is it will be useful to others to help learn math and prove new theorems.