Klaus Grue (invited talk)
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
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
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
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
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
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
talk/demo on Wikicoqweb: Proofs for freshmen with Coqweb
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.
Formal Reasoning with Different Logical Foundations
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
Asynchronous processing of proof documents --
rethinking interactive theorem proving
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
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"
- The prover should be able to re-order and re-schedule individual
theory and proof transactions according to their inherent
- 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
- 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.
Collaborative Editing with PGIP
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
Challenges to a global web-based library of formal mathematics
(Based on discussions with Cezary Kaliszyk and Pierre Corbineau)
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
- 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.
Documenting and Editing Formal Mathematics in Natural Language
- GF: translations between languages (both formal and natural)
- GF Resource Grammar Library: high-level programming of
grammatically correct translation rules
multilingual syntax editors from GF grammars
Teaching logic using a web interface for Coq
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.
A prototype system for collaborative proving
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.
An Implicational Logic for Conjecturing and Distributed Proof Attempts
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.
A glimpse of Evgeny Makarov's abstract and modular
formalisation of arithmetic in Coq
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
Obstacles to a global library of formal mathematics
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.
Providing mathematical Web services with Symbolic Computation
Software Composability Protocol
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
- 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
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
Back to MathWiki main page
Last modified: Mon Nov 19 13:49:21 GMT 2007