Antoine Leudière

Miscellanea

Education

  • 2021-2024. PhD Thesis: Drinfeld modules algorithmics and post-quantum cryptography. Advisors: Emmanuel Thomé and Pierre-Jean Spaenlehauer. INRIA CARAMBA, Nancy, France.
  • 2020-2021. MsC 2nd year. Applied algebra. Université Paris-Saclay.
  • 2019-2020. MsC 1st year. Mathematics and applications. Sorbonne Université.
  • 2018-2019. BsC 3rd year. Mathematics and applications. Sorbonne Université.
  • 2015-2018. BsC. Music and Musicology. Sorbonne Université.
  • 2015-2018. BsC. Mechanics. Sorbonne Université.

Ktorphée

Je suis impliqué dans le séminaire de mathématiques libre et sous-terrain Ktorphée.

(I am involved with the free and underground mathematics seminar Ktorphée.)

dEAduction

I co-created and co-wrote dEAduction (all original ideas and developement by Frédéric Le Roux) a program that teaches undergrad students some aspects of mathematical reasoning. By augmenting the theorem prover LEAN with a (hopefully!) intuitive graphical interface, we aim at convincing students that some elementary — almost automatic — demonstrations require basic deductions but almost no creativity. For example, in a metric space, the open balls are open. To prove this, you take an epsilon (automatic step), then you know (because of the ‘exists’ in the definition) that you have to find a certain radius. The good value of the radius is found by stripping down step by step the definition of being open. Of course, mathematics cannot be reduced to automatisms, and dEAduction is to be used with pedagogical finesse.

The benefits of using LEAN is that a student can never prove something wrong, which, in itself, is pedagogically useful. A teacher can create full courses that take advantage of dEAduction, by “simply” writing native LEAN files. There are several modes available.

dEAduction has been tested in real conditions, with very good outcome; see this report (French) by Camille Lichère. The program is, however, not ready for large scale deployment. We need backup on the installation aspects. The license is GNU GPL v3; help of any kind would be welcome with open arms.

On a technical point of view, I designed and wrote the first version of the graphical interface, and helped on some other aspects. For this work, I was employed by Sorbonne University.

The original idea was by Frédéric Le Roux (IMJ-PRG, Paris), a great mathematician, teacher and human-being, who remains the most important member of the project.

Music

I play the violin, and a little bit of bass and guitar; get in touch if you want me to bring my folk guitar to conferences.