Making proofs by hand: attempt for a novel interface for Coq
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.
Interactive Authoring of Terrain using Diffusion Models
Generating heightfield terrains is a necessary precursor to the depiction of computer-generated natural scenes in a variety of applications. Authoring such terrains is made challenging by the need for interactive feedback, effective user control, and perceptually realistic output encompassing a range of landforms. We address these challenges by developing a terrain-authoring framework underpinned by an adaptation of diffusion models for conditional image synthesis, trained on real-world elevation data. This framework supports automated cleaning of the training set; authoring control through style selection and feature sketches; the ability to import and freely edit pre-existing terrains, and resolution amplification up to the limits of the source data. Our framework improves on previous machine-learning approaches by: expanding landform variety beyond mountainous terrain to encompass cliffs, canyons, and plains; providing a better balance between terseness and specificity in user control, and improving the fidelity of global terrain structure and perceptual realism. This is demonstrated through drainage simulations and a user study testing the perceived realism for different classes of terrain.
Analog computing is back
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.