Hacker News new | past | comments | ask | show | jobs | submit login

Nice project! I'm working on something similar with http://fungrim.org/grim/ and http://fungrim.org/



Pretty cool. Are you aware that there is a content markup part of MathML https://www.w3.org/TR/MathML3/chapter4.html ? There are other efforts geared towards math authoring as well if that is your focus,for example people have authored open textbooks using https://pretextbook.org .


Indeed. I decided not to use MathML for various reasons:

1. The syntax is horrible (for writing by hand).

2. I'm more interested in computation than presentation, so something closer to S-expressions along the lines of Mathematica feels more comfortable to me.

3. The progress so far on defining semantics for content MathML has failed to impress me.

Concretely, I think if you are trying to do semantic mathematics, you need an implementation of the semantics in software, not just a hand-written spec. Ideally this would be backed by a formal theorem proving system. So far I just do randomized testing using symbolic evaluation and interval arithmetic. See this writeup for more details: https://arxiv.org/abs/2003.06181


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.


Thanks! The symbolic computation aspect of your paper is very interesting. I would be very interested in checking out how conditional rewriting is achieved. Do you have more in depth writings on the theory and mechanics of your approach?


There is nothing in depth yet. I'm happy to discuss (here or by email).


Cool. I have skimmed through the code base. I will email you with further questions.


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.


Sure, go ahead and set something up!


Cool. I've setup a Google Group at https://groups.google.com/d/forum/mathlingua-discuss.


Yes that would be nice. Thanks!


Awesome. I've setup a Google Group at https://groups.google.com/d/forum/mathlingua-discuss.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: