Interactive formal proofs systems like HOL, Isabelle, Lean or Coq have generally two levels of language:

• One is the language of mathematical objects and statements. These go from « 2+2=4 » to the most complex theorems.

• The second is a language to allow the user to progressively construct mechanically verified proofs of these statements. Very often this is a kind of script language built around basic commands called « proof tactics ».

Learning and mastering this proof language is difficult. One can consider this to be a hinderance for a wider use of proof systems; especially in education but also in the mathematical community in general.

I will present and demonstrate the prototype of Actema, a novel user interface for building formal proofs without text but through gestures on the screen. We hope this approach is a step towards more intuitive and easy to use proof systems.

More specifically, I will present a version of Actema which acts as a front end to the Coq theorem prover.

I will also present the logical mechanisms at play, which involve the approach called Deep Inference, and say a few words about how the gestures are translated into Coq proofs terms.

I hope this to be an entertaining talk, and am curious about the feedback from the audience.

A first version of the interface is accessible on-line on: http://actema.xyz/

The version I will show is more advanced, because it relies on Coq as a back-end.

This is joint work with Kaustuv Chaudhuri, Pablo Donato and Pierre-Yves Strub.