Contexte et atouts du poste

Whale est un projet d'assistant de raisonnement formel accessible, utilisable directement dans le navigateur. Notre but : permettre aux personnes dans les domaines scientifiques, en recherche et en ingéniérie de vérifier rigoureusement un calcul, un raisonnement ou une démonstration sans avoir besoin d'une formation spécialisée.

Nous souhaitons qu'un(e) ingénieur(e) en biologie puisse vérifier formellement un protocole experimental en 2 jours, et dans son propre jargon, quand il aurait fallu un mois de collaboration avec un expert en méthodes formelles par le passé. Qu'un chercheur en psychologie puisse s'assurer qu'un raisonnement statistique tient debout avant publication, etc. C'est ce que rendent possibles les assistants de preuve modernes. Mais ils sont aujourd'hui réservé à une poignée de spécialistes.

Whale souhaite rendre la rigueur de ces assistants (Rocq, Lean, Isabelle, Agda) accessible dans le langage m...