Megalodon 1.4

by Brown, Thursday, February 04, 2021, 17:21 (304 days ago)

Megalodon 1.4 is ready:

http://grid01.ciirc.cvut.cz/~chad/megalodon-1.4.tgz

Since there were some problems with the formulations of some conjectures in 1.3, I spent some time defining a "real number structure" following Dieudonne's Foundations of Modern Analysis. So now it's possible to assume one has an abstract real number structure and then make definitions/prove theorems relative to that structure. I carved out natural numbers, integers and rational numbers from such a real number structure, so now to say "the set of rational numbers is denumerable" one can say "for every real number structure Rs, the set of rational numbers Q derived from Rs is denumerable." I added a file form100_R1.mg that reformulates some of the "Top 100 Theorems" in this style.

I also went through Section 2.2 of Dieudonne's book and formulated the 17 theorems there (and a couple of little facts) as 41 conjectures. (Many "equivalence" theorems will be easier to apply if they are a sequence of separate results.) They should be relatively easy to prove, once someone gets the hang of proving in Megalodon.

I also conjectured that the quotient of a group by a normal subgroup is a group and that the canonical map is a group homomorphism. These should be easy but tedious facts to prove.

A nice thing about old math books like Dieudonne's is that with a bit of searching anyone can find a copy online for free. If you want to formally prove some of the conjectures, the informal proofs in Dieudonne's book would likely be helpful.