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.

The idea of considering analog models of computation (by opposition to today’s digital models) is not new, and actually the first ever built computer were analog. Some well-known models of analog computers have been proposed, such as the GPAC (General Purpose Analog Computer) of Claude Shannon in 1941. However, these models have been mostly forgotten as they were 1) thought to be less powerful than a modern computer 2) not as good as modern computers for doing precise computations.

But it turns out that 1) is wrong, and this was proved only a decade ago, and analog computers could even solve some problems faster and 2) that many modern applications of computers are precisely contexts, such as machine learning or deep learning, where precision is not so important. What matters most is speed and energy consumptions, which are precisely the strength of analog computers.

Actually, analog computing comes historically also from the idea of computing by analogy. We will review various recent rebirth of analog computing and analog models, including recent startups proposing very fast computing for deep learning, or (re)birth of models based on analog computing, such as neural ordinary differential equations, or explanations of performances of some digital models through the eyes of analog computing.