Since the formalism for encoding knowledge in the hyperreal dictionary is to be based as much as possible on the practise of mathematicians, we need to examine samples of mathematical writing as the "raw data" from which to build our theories. Already, there is a collection of a hundred definitions which Joe has translated into a mocked-up preview version of h-code, by hand.
In addition to definitions, it would be nice to have some similar examples of proofs which have been translated into h-code by hand. We already have two such examples — a proof of Beatty's theorem and a theorem on cosets, but it would be nice to have more. Since proofs tend to be longer than definitions, not so many would be neeeded, perhaps a dozen or so proofs would be a good start. Naturally, more would be welcome, and, as the project advances, more proofs and definitions will surely be translated.
Note, writing up proofs in a language still under development is something of a chicken and egg problem. A reasonable way to start would be to write the proof as it would appear in a textbook or homework solution, then progressively formalize; see Levels of Proof Checking. In a sense, you'll be simulating steps that the parser may take - so document your process!
Note also that these proofs can use definitions from the Hcode libraries (even made up definitions that haven't been written yet).
See also "experiment with automated proofs of various interesting facts" and other pages from JACKYL for ideas of things to work on writing up in hcode. The proof that ten is even seems like a reasonable start (remember, we're just trying to do the hcode). --jcorneli Thu Feb 10 12:08:20 2005