4 ms·

Documenting mathematics rigorously is actually hard. For example see the Formal Abstracts (https://formalabstracts.github.io https://formalabstracts.github.io)

Documenting mathematics rigorously is actually hard. For example see the Formal Abstracts (https://formalabstracts.github.io https://formalabstracts.github.io) project by Thomas Hales. Hales' other writings on the subject may be informative too: https://jiggerwit.wordpress.com/2019/06/20/an-argument-for-controlled-natural-languages-in-mathematics/ https://jiggerwit.wordpress.com/2019/06/20/an-argument-for-c...

CatsAreCool 6y ago
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.
- fspeech 6y ago
  This is an area of my interest too, esp. if one can find something that is actually useful for a practicing mathematician. I mentioned Hales' project but based on their github project progress (a postdoc of his did some exploratory work) they seemed to have hit some road blocks, which is an example of this problem being hard. I don't know what your background is. If you are interested in further discussion I would be happy to p.m. over email.
  - CatsAreCool 6y ago
    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 https://github.com/DominicKramer. Let me know if you have problems getting it.
- ratmice 6y ago
  This also reminds me of mmt https://uniformal.github.io/ https://uniformal.github.io/ The primary developer of that recently gave a talk about it here https://vimeo.com/421123419 https://vimeo.com/421123419
jhanschoo 6y ago
Also see: https://en.wikipedia.org/wiki/QED_manifesto https://en.wikipedia.org/wiki/QED_manifesto
- CatsAreCool 6y ago
  I have read through this before, but thanks for sharing the link.

CatsAreCool 6y ago

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.

fspeech 6y ago
This is an area of my interest too, esp. if one can find something that is actually useful for a practicing mathematician. I mentioned Hales' project but based on their github project progress (a postdoc of his did some exploratory work) they seemed to have hit some road blocks, which is an example of this problem being hard. I don't know what your background is. If you are interested in further discussion I would be happy to p.m. over email.
- CatsAreCool 6y ago
  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 https://github.com/DominicKramer. Let me know if you have problems getting it.
ratmice 6y ago
This also reminds me of mmt https://uniformal.github.io/ https://uniformal.github.io/ The primary developer of that recently gave a talk about it here https://vimeo.com/421123419 https://vimeo.com/421123419

jhanschoo 6y ago

Also see: https://en.wikipedia.org/wiki/QED_manifesto https://en.wikipedia.org/wiki/QED_manifesto

CatsAreCool 6y ago
I have read through this before, but thanks for sharing the link.