We have formally defined and proven theorems about Conway's
surreal numbers (a generalization of both real numbers and ordinal
numbers) in a higher order set theory.

Formalizing such mathematical notions involves more than simply making
definitions and finding proofs of theorems.

Definitions and proven theorems must be integrated into a library
others can build upon.

A blockchain associated with a cryptocurrency and peer to peer network
is analogous to a book into which anyone can publish a new chapter, as
long as what is written is consistent with the rules of the network.

In the Proofgold network the rules allow anyone to publish definitions
and proofs of theorems, as long as they are new and correct, giving a
new (and very open) way of publishing and building upon formal
mathematics.

Our construction of Conway's surreal numbers and the relevant proven
theorems have been published into the Proofgold blockchain so that
notions depending on the real numbers (or more generally on surreal
numbers) now can also be published into the blockchain.