Megalodon 1.8

by Brown, Friday, November 26, 2021, 18:05 (9 days ago)
edited by Brown, Friday, November 26, 2021, 18:09

Here is Megalodon 1.8:

This version includes a formal construction of real (and complex) numbers via Conway's surreal numbers. All of it has been published into the Proofgold chain.

I also created an html/javascript presentation of the formalization split into 9 parts:

Basic Infrastructure:

Surreal Numbers as an Ordinal and a Predicate:

Surreal Numbers as Sets:

Unary Minus:



Integers and Diadic Rationals:



For most proofs there is an option to prove the theorem (often split into multiple goals) in a javascript interactive tableau theorem prover. The prover is classical, so the correspondence to Proofgold really only makes sense after excluded middle is proven early in Part 1 (via Diaconescu). The html/javascript files are available together here:

I've often gotten the feedback that my websites are "old-looking" so if anyone wants to download the collection and do fancy tricks to give it a facelift (i.e., make it look like people expect Google/Facebook/Twitter to look), then feel free.

Complete thread:

 RSS Feed of thread

powered by my little forum