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...
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.