💾 Archived View for dioskouroi.xyz › thread › 29419039 captured on 2021-12-03 at 14:04:38. Gemini links have been rewritten to link to archived content

-=-=-=-=-=-=-

Show HN: MathLingua – A Structured Language of Mathematics

Author: CatsAreCool

Score: 93

Comments: 23

Date: 2021-12-02 17:12:42

Web Link

________________________________________________________________________________

CatsAreCool wrote at 2021-12-02 22:08:25:

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.

triclops200 wrote at 2021-12-03 01:15:13:

Awesome project: I love the fact that you can click grab definitions, would make learning new symbols in a field a breeze.

Question, though: is there a way to add custom definitions to symbols when you work in a field that uses symbols differently than the standard usage or symbols that have no standard usage (such as \bigoplus in latex)?

CatsAreCool wrote at 2021-12-03 02:38:29:

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.

triclops200 wrote at 2021-12-03 14:36:21:

Awesome! Sounds like a great system

CatsAreCool wrote at 2021-12-03 02:40:03:

I haven’t added a reverse lookup yet where you provide a symbol and can find all things that the symbol can represent, but it is on the roadmap.

robinzfc wrote at 2021-12-03 08:17:03:

This is very similar to Isabelle's Isar [1], except that Isar definitions and theorems can be formally verified.

MMathLingua has no doubt a much better presentation layer for mathematics than Isabelle/Isar. This can be improved with a custom presentation layer, see for example rendering of topological groups theory from IsarMathLib [2] written in Isar (disclaimer - my project).

[1]

https://isabelle.in.tum.de/Isar/

[2]

https://isarmathlib.org/TopologicalGroup_ZF.html

est wrote at 2021-12-03 06:10:19:

The next natural step would be write down all theorems from kindergarten to undergrad and make them reproduciable with

http://leanprover.github.io/

vixen99 wrote at 2021-12-03 09:18:03:

One could start with the almost 1000 pages of George Shoobridge Carr's _a synopsis of elementary results in pure mathematics_ published in 1837. If someone were to update this book for 2021 I'm curious to know how many pages that might run to.

silasdb wrote at 2021-12-03 11:17:35:

Great project. BTW, I'm more and more interested in how to produce math for blind people. Although there is some recommendation about writring math in MathML, few (none?) screenreaders actually support it. Could this project help or could you tell me other resources about it? Thanks.

CatsAreCool wrote at 2021-12-03 18:51:21:

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.

chriswarbo wrote at 2021-12-03 09:20:56:

Seems similar to

http://openmath.org

e.g.

https://www.omdoc.org/about/

https://kwarc.info/systems/sTeX

CatsAreCool wrote at 2021-12-03 18:59:22:

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.

clavalle wrote at 2021-12-03 05:06:00:

I come from a very practical engineering math background.

I am really excited about this project because it makes it very clear how everything hangs together in a way that I haven't experienced before. The visual structure of a single definition/theorem/states is very helpful. Also, knowing how many 'levels' from the original concept I'm currently exploring while unpacking and re-packing just helps everything click into place.

Very, very cool.

igorkraw wrote at 2021-12-03 07:44:18:

Does this handle ambiguity in definitions/standardization of expressions? Like, if I define entropy H(q,p) with mesures q (X), p(X) and with mesures a (y),b(y) , can I use the mathlingua parser to abstract this to the same representation? Or is it strictly a presentation layer?

crvdgc wrote at 2021-12-03 01:51:03:

This is great. You can easily look up a definition within a definition. No more context switching when trying to find Theorem 17.23, and then Definition 2.7.

CatsAreCool wrote at 2021-12-03 02:42:23:

I’m glad you like it. One of the goals is to make discovering math easy and fun, in particular exploring theorems and definitions.

gnull wrote at 2021-12-03 12:21:38:

So is it like math written in natural language but more structured and cross-referenced?

CatsAreCool wrote at 2021-12-03 18:54:52:

That is correct, and the structure allows for computers to better understand the meaning of the math concepts being described, which opens the door to different analyses that can be done.

cloudhan wrote at 2021-12-03 06:59:30:

I think you might be interesting in this interactive papar:

https://willcrichton.net/nota/

CatsAreCool wrote at 2021-12-03 18:53:07:

Looks interesting. Thanks for the link.

mkl wrote at 2021-12-03 07:45:50:

I think you have a typo in the front page example. It says "F(x) is indefinite integral of f(x) on A", but the interval is "I".

derived_lush wrote at 2021-12-03 09:44:52:

Have you thought about using madoko [1] as a backend for math rendering?

Madoko has great support for rendering maths for the web, by far superior to KaTeX and MathJax.

[1]:

http://madoko.org/reference.html

tombert wrote at 2021-12-03 05:33:12:

Oh my goodness, this is awesome. It's like the tactics language of Coq, but less irritating and pretty formatting. I will be recommending this to everyone!