One would have expected that all of mathematics would have been machine 
formalized some decades after the invention of the digital computer. But 
it seems that something has been missing for that to happen.

Logiweb (http://logiweb.eu/) was conceived in an attempt to analyse what 
was missing. And it was designed and implemented 1996-2006 to meet the 
following objectives:

Accumulation of knowledge: Once a machine formalized development was 
published on Logiweb, the publication should remain accessible in 
unchanged form forever. This simply mimics what publishing houses and 
libraries provide for ordinary mathematics.

Standing on the shoulders of predecessors: When proving a theorem, users 
should be able to draw upon theorems proved by others. This simply mimics 
the way any mathematician works.

Notational freedom: Each user should be free to use any notation. That 
freedom should come without restricting the notational freedom of others. 
And differences in notation should be no obstacle when using the results 
of others.

Foundational freedom: Each user should be free to choose what mathematical 
foundation to work upon. Import of results from one foundation to another 
should be possible (but not neccessarily trivial).

Distribution: Access to the work of others should happen transparently via 
the Internet.

Readibility: Users should be able to publish articles on Logiweb which are 
as readable as any mathematics book one can pick from any library.

Accommodation: Users should be able to publish anything from short notes 
to multi-volume works that span thousands of pages.

Scalability: The system should allow an arbitrary number of submissions 
and should run smoothly up to 10^18 papers.

Simplicity: The system should be so simple that its core could be 
implemented by a single person. And so simple that once it was 
implemented, a graduate computer science student could re-implement it in 
one year.

Extensibility: Once the core was implemented, users should be able to 
adapt the system without changing the core and should be able to publish 
adaptations on Logiweb itself to make the adaptations available to other 
users.

Verification: Logiweb should be able to tell whether or not a publication 
is correct. In the spirit of accumulation, correctness should be time 
independent such that a publication which is deemed correct at one time 
should remain correct forever.

Logiweb is a rather simple system which fulfills the objectives above. The 
talk gives a walk-through of the system. Furthermore, the talk describes 
how Logiweb can interface to other systems like wiki systems and other 
proof systems.

Coqweb is a web interface for Coq, primarily designed for teaching. It
allows teachers to propose statements in sufficiently familiar
form. Students are invited to prove these statements essentially by
clicking. Hints can be given in natural language, in which case the
interface checks that the student somehow understands the hints. We
present here the main features of Coqweb, and show through examples
how it has been used since 2004.

We will present the key aspects of the Mizar technology for formalizing
mathematics as well as building and maintaining a database of formalized
and semantically linked knowledge - Mizar Mathematical Library. We will
focus on the issues relevant to the WWW environment: XML-based
presentation, querying with MMLQuery and on-line processing of Mizar
documents.

The classical model of interactive proof-checking is best illustrated by 
the de-facto standard user-interface, namely Proof General. Here the user 
operates on a collection of theory files, while editing the body of a 
single theory works by stepping back and forth in a strictly sequential 
(synchronous) fashion.

I would like to take a fresh look at how proof documents are processed. 
Both the increased demands of large formalizations should be addressed, as 
well as multi-processing that has become readily available now. 
Ultimately, user-interfaces and related prover protocols with the 
following characteristics should emerge:

  - Less requirements on the "editor" component, i.e. make it work with 
    simple web interfaces, rather than demanding a "rich client" 
    architecture.
  - The prover should be able to re-order and re-schedule individual 
    theory and proof transactions according to their inherent 
    dependencies.
  - The user should be able to edit theory sources very freely, with the 
    system maintaining consistency as expected. Here the inherent 
    structure of a proof language like Isar admits the outline to be 
    checked quickly, while the sub-proofs may be refined later by 
    iterative deepening.
  - Editing of unfinished, partially broken theories and proofs should be 
    easy (in fact the norm rather than the exception).

Thus we hope to increase effectiveness of interactive theorem proving 
significantly, enabling users to work on much larger formalizations.

We will give a fresh view on the display side of the PGIP protocol,
which connects interface front-ends (called displays) with the central
PGIP middleware (and hence the provers). This stateless display protocol
can be conveniently modelled as a REST-style interface with XUpdate
messages signalling changes. From there, we discuss possibilities for
collaborative editing in this context-- it turns out that collaborative
editing is more or less built in, but needs to be restricted to make it
useful.

I will discuss what I perceive to be the possibilities for developing a 
"Wiki for Formalized Mathematics" within a joint European ICT project.
I see two main motivations for such a system:
- Cooperative work on a large repository of formalized mathematics. This 
is also to solve the problem that "there is not enough mathematics 
formalized".
- Providing high level access to a repository of formal maths. When 
searching for a mathematical notion, one should also get a 
comprehensible link to the formalization. This should also help solve 
the "access problem": what is in the repository?
In the talk I will discuss what could be done and what I think should be 
done. Audience participation during the talk is very much appreciated.

- GF: translations between languages (both formal and natural)
- GF Resource Grammar Library: high-level programming of  
grammatically correct translation rules
- embedded grammars in JavaScript: automatic generation of  
multilingual syntax editors from GF grammars
- using embedded JavaScript grammars in Wiki pages

We will present the system ProofWeb, that allows teaching students
logic using an interactive web interface to the proof assistant Coq.
First we will present a general framework for creating responsive web
interfaces to proof assistants, which allows the students to use the
system without the need to install anything (not even a browser
plug-in). On top of that we will present an extension for teaching,
that makes the full power of Coq available to the students, but
simultaneously presents the logic problems in a way that is customary
in undergraduate logic courses. Both styles of presenting natural
deduction proofs (Gentzen-style `tree view' and Fitch-style `box
view') are supported. The system allows the teachers to centrally
track progress of the students. We will present a database of logic
problems, that also holds the students solutions and a parser that
indicates whether the students used only the allowed inference rules
of the logic.

We present a framework for the online development of formalized
mathematics. This framework allows wiki-style collaboration while
providing users with a rendered and browsable version of their work.
We describe a prototype for Coq, based on the web interface
implemented by Cezary Kaliszyk (which he will present in his talk),
and a modified version of the MediaWiki code-base.

Then, we will focus on cross-file consistency and dependency issues
with concurrent access and write, and finally on requirements for
supporting existing proof assistants.

I will introduce a logic of implication which supports making
conjectures as a basic operation. This allows them to be used before
they are proved as well as reused in different branches of a proof and
in different parts of a theory. This forms a meta-theory for theories
which allows distributed proof attempts while maintaining the
interdependencies between lemmas. I hope to develop this into a full
type theory which gives keeps support for distributed development.

Evgeny Makarov formalised basic axiomatic arithmetic in Coq.  He came
up with two sets of Peano-style axioms that characterise respectively
natural numbers and integers and differ only in saying whether every
number has a predecessor. Then he derived generic lemmas about "plus",
"times", "less than" and a setoid equality. New functions can be
defined generically using Peano's recursion or by axiomatising their
defining properties and providing implementations of these properties
for various datatypes (zero-and-successor numbers, binary numbers,
etc.). Theorems proved from defining properties hold for every
implementation. Automation such as polynomial simplification (the ring
tactic) directly hold from the genericity of Barras-Gregoire-Mahboubi
implementation. Generic decision of linear arithmetic (and beyond), is
work in progress.

From the "math wiki" perspective, we wonder whether focusing on a
well-delimited mathematical theory such as the one used to formalise
arithmetic, or more generally number theory, could provide an
interesting first step to make both human beings and the different
proof assistants agree on a common high-level domain-specific
mathematical vernacular.

I will discuss what I perceive to be the main reasons that there is
not yet a large scale effort to create a good and comprehensive
library of formal mathematics.

Modern symbolic computations require infrastructure for parallel
algorithms and combining capabilities available in several different
systems.  Moreover, there are growing numbers of symbolic computation
resources, such as databases or specialised software which could be
made available as Web services or Grid services accessible over the
Internet.  The EU Framework VI project "SCIEnce --- Symbolic
Computation Infrastructure in Europe"
(http://www.symbolic-computation.org/) addresses these needs of the
symbolic computation user community.

First we designed the Symbolic Computation Software Composibility
Protocol (SCSCP) by which a computer algebra system (CAS) may offer
services and a client may employ them. We envisage clients for this
protocol including:
- A Web server which passes on the same services as Web services
using SOAP/HTTP protocols to a variety of possible clients;
- Grid middleware;
- Another instance of the same CAS (in a parallel computing context);
- Another CAS running on the same computer system or remotely.
All messages in the protocol are represented as OpenMath objects
(http://www.openmath.org).

In my talk I will give more details about OpenMath and SCSCP, and will
demonstrate some examples using SCSCP implementation for the
computational algebra system GAP (http://www.gap-system.org).

Other people who will attend