List view

• 4. Efficient proof input

  Includes automated proof search and an integrated computer algebra system.

  No due date

  •0/9 issues closed
  0% complete9 open0 closed

• 3. Complete implementation of HLM rules

  Besides type and proof checking, also includes a complete implementation of the non-circularity rules.

  No due date

  •2/8 issues closed
  25% complete6 open2 closed

• 2. Web-based proof input

  Everything that's necessary to enter proofs via the web GUI.

  No due date

  •1/6 issues closed
  16% complete5 open1 closed

• 1. Web-based input of definitions and theorem statements

  This is the bare minimum that is required for others to meaningfully contribute to the library. Incorporates both the input via the GUI and the necessary type checking, but no proof input. Most of this has already been implemented in the desktop version.

  No due date

  •17/28 issues closed
  60% complete11 open17 closed