# User:Kingdon

Hi, I contribute to wikiproofs and this page contains a few of my thoughts, todo items for myself, and other stuff I haven't found a better place for.

## Three Challenges[edit]

The three hard parts of a formalized math project (in my view) are (1) make it sufficiently easy to read and write proofs, (2) attract a large enough body of contributors to spread the work so you don't burn out like Whitehead and Russell did (they wanted to spend one year on *Principia*, and it took ten), and (3) formalize a large enough body of known mathematics that proofs don't need to rederive a lot of known results just to get started.

The current situation (again, as far as I can tell): (1) there has been a lot of attention to new proof engines and proof languages, but it still warrants further work and experimentation, as I have yet to see a system which I *really* like. (2) there are a huge number of systems with just one contributor, or a small number (I frequently discover new ones). In one sense this is promising, as it indicates interest, but just highlights the challenge of attracting people to a project, which is also related to items (1) and (3). Metamath is perhaps the closest to having a diverse set of participants. (3) Some of the Isabelle libraries perhaps come closest to this one.

## Experimental pages[edit]

## Geometry[edit]

Do we want/need/know how to get more familiar notation such as the line AB, the angle ∠ABC, the triangle △ABC, etc?

Don't yet know if this is easy or hard, but the 17-gon might be a cute result to prove.

## First order logic todos[edit]

- Not sure whether these are the most salient subst theorems (perhaps better to see what we end up needing), but some interesting-looking ones are:

- Follow up on Foo -> FooNotFree rename per Interface talk:First-order logic.