Megalodon 1.4

by Brown, Thursday, February 04, 2021, 17:21 (234 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.

RSS Feed of thread
powered by my little forum