# About

## Actema is an experiment in GUIs for proof assistants.

It all started with the following question:

*Do we need textual commands to build formal proofs?*

A first answer was provided by the
Proof-by-Pointing effort in the 90s, where the simple act of
*pointing* at parts of logical expressions was identified as
a powerful mechanism for performing basic reasoning. This is in
contrast with traditional *proof scripts*, where the user
needs to know the syntax of various unrelated *tactics*
before she can start writing proofs.

The Actema project can be seen as a direct continuation of
Proof-by-Pointing. Its goal is to develop principles to handle
graphically most aspects of proof development beyond basic
reasoning. Currently, we explore new ways of interacting through
direct manipulation with various objects of mathematical discourse:
propositions, equations, definitions, lemmas...

## The Actema Team

This is an effort initiated by the Typical team of the
LIX laboratory. Active developers are
Pablo
Donato, Pierre-Yves Strub and
Benjamin
Werner.

Front-end and website realized by Sébastien Najjar from Dioxygen Software.