Forum de mathématiques - Bibm@th.net

Arnaud88

Invité

Assistant de preuves.

Bonjour,

Est ce que vous pouvez m'expliquer comment fonctionne l'assistant de preuves en mathématiques, qui se trouve sur le lien suivant : https://leanprover-community.github.io/
Mon niveau en anglais n'est pas très fort.
Comment je peux demander ou collaborer avec ce site afin qu'il me fournit les clés de démonstration autour d'un problème en mathématiques.
On m'a dit que ce site ci-dessus est fait pour ça.

Merci d'avance.

Omhaf

Membre

Inscription : 16-01-2020

Messages : 286

Re : Assistant de preuves.

Bonjour à tous
Avant que je lise ce que dit le site que tu as mentionné, je pourrais te rappeler que les outils de traduction anglais-français sont disponibles sur le net
Si malgré la traduction tu n'arrives pas à saisir le fonctionnement , là certains amis pourraient intervenir s'ils le souhaitent
Bonne chance !

yoshi

Modo Ferox

Inscription : 20-11-2005

Messages : 17 385

Re : Assistant de preuves.

Bonsoir,

Alors, le meilleur traducteur Internet que je connaisse est deepL.
Dans sa version gratuite, il est limité en nombre de caractères, 500 il me semble...
Limitation facilement contournable : il suffit de réfléchir un peu pour trouver...
Ce qu'est un "Assistant de preuve".
Par exemple LEAN : https://fr.wikipedia.org/wiki/Lean_(ass … de_preuve)

Sinon, un mien neveu, féru de programmation, m'avait parlé d'un langage de programmation assez différent des classiques, Delphi, Python, C et ses variantes, R, Rust ou encore Java  : coq qui permettait de valider l'exactitude de démonstrations de théorèmes !
Il le pratiquait et j'avais pensé, comme il bossait sur une IA chez Micro$oft (oui, le dollar est une "coquetterie" de ma part), qu'il devait savoir de quoi il retournait...
Et effectivement on ressort de ces lectures quelque peu impressionné :
https://zestedesavoir.com/articles/3758 … -avec-coq/
https://www.labri.fr/perso/casteran/FM/MTOCPL/JDEV.pdf
ou encore :
Théorème des 4 couleurs (vérification de la validité de la preuve...)

Maintenant, pour qui veut se lancer dans des stages, mieux vaut ne pas être smicard ou avoir gagné une grosse somme au Loto :
https://www.inria-academy.fr/formation/ … -logiciel/

@+

Dernière modification par yoshi (07-10-2024 09:13:22)

Zebulor

Membre expert

Inscription : 21-10-2018

Messages : 2 220

Re : Assistant de preuves.

Bonjour,

Alors, le meilleur traducteur Internet que je connaisse est deepL.

@+

Je confirme pour l'apprentissage du russe !