Metamath (programming language)

Post Reply New Topic

Hello everyone.

Upon searching for research papers concerning the field of metamathematics, I discovered, quite serendipitously, a mathematical curiosity that I think deserves the attention of the people of Wrong Planet. I found a tiny programming language -- called Metamath -- that serves the purpose of checking and producing logical/mathematical proofs. I clicked on the link to the main Metamath website, and found the program, compiled it, and am viewing it using QT. There is so much I could tell you, but I'm going to save myself a lot of typing and formulating sentences by providing you with the Wikipedia page for Metamath, as well as the Metamath website.

Wikipedia: Metamath

Metamath Homepage

Check them out!

cool, thanks for sharing!

That is pretty cool, thanks!

Checked out your website too, really cool to see someone else into Gregory Chaitin.

I am studying philosophy, but am pretty much interested in everything you list. I am studying philosophy because it has a real potential to be cross disciplinary and guide research in places where scientists are really confused, eg, Consciousness.