Formalpedia is an “editable online repository of code and formal math”. It is on its way to become the first formalized mathematics wiki that goes online. Formalpedia is still read only, so it is not there yet. Mathematics on Formalpedia is (to be) verified by HOL Light. Most of the proofs are “not available yet”, but there are a couple that have been imported, so one can get the idea for how the presentation looks like. HOL Light verification scripts are known to be mostly write only, but one can see that the web presentation can help a lot in this respect. Formalpedia does use some mathematical notation and provides links to the “tactics” referenced in proofs. The assertion of a typical theorem looks like this:

Theorem (fact_divides_thm).

\forall m\; n.\; m \leq_N n \Rightarrow (\exists d .\; Arith.fact\; n = d\times_N Arith.fact\; m)

As we can see there is some confusing “Arith.fact” noise. Also for the theorem to be true the relation “m\leq_N m” would have to somehow imply that m,n are elements of some field. To understand how this happens I tried to click on \leq_N symbol, but that does not lead to the definition of that symbol, but rather to the whole rather big file where I guess the definition is. But with proper links to definitions and some effort from the reader I believe verification scripts presented at Formalpedia can be converted into readable proofs. Allowing informal (but LaTeX enabled) text to be interleaved with the formal HOL Light text would greatly improve readability of mathematics for people who are not HOL Light users. Clickable symbols in mathematical formulas is a very good idea and I would like to have something like that in IsarMathLib presentation at as well. I don’t think jsMath that displays the math there supports that though.

Formalpedia is clearly under development and it is good that the authors (author?) decided to post this early alpha version. It would be better if they provided an easy way for getting a feedback from viewers. I could not find any link to a forum, blog or even e-mail that would allow for that. Maybe I missed something.


Tags: , ,

2 Responses to “Formalpedia”

  1. anon Says:

    A little bit of research shows that the Formalpedia project was started by Jeremy Bem @ . The project seems to be in its early stages, but I agree with you about the lack of any venuee for feedback.

  2. Jeremy Says:

    Hi – thanks for the interest! I’ve just resumed work on Formalpedia after a several month hiatus. The “Arith.fact” noise has been cleaned up and a discussion forum has been added, among other improvements; many more are on the way. Feedback is welcome and appreciated. ~Jeremy

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.

%d bloggers like this: