Comment Jules, 15 ans, a redécouvert les relations de Viète
Mon fils m'a récemment présenté une formule mathématique qu'il avait trouvée par lui-même. Il s'ennuyait en cours de maths et, il a élaboré un solution à un problème : comment retrouver deux nombres quand on connaît seulement leur somme et leur produit ?
Sa solution :
x = S/2 + √(S²/4 - P)
y = S/2 - √(S²/4 - P)
où S est la somme et P le produit des deux nombres recherchés.
Intrigué par sa découverte, j'ai voulu vérifier formellement sa démonstration en utilisant un assistant de preuve mathématique. Cet article raconte notre démarche.
Le raisonnement de Jules
L'intuition géométrique
Jules a imaginé le problème à partir d'un grand carré. Son raisonnement était le suivant :
« La somme de deux nombres, c'est forcément égal à la moitié plus quelque chose, plus la moitié moins quelque chose. Du coup on peut barrer les écarts quand on fait la somme. Mais ces écarts sont utiles pour trouver le produit. »
En termes mathématiques, il a posé : – x = S/2 + d (la moyenne plus un écart) – y = S/2 – d (la moyenne moins le même écart)
Pourquoi ça marche pour la somme
x + y = (S/2 + d) + (S/2 - d) = S
Les écarts +d et -d « se barrent » — c'est exactement ce qu'il avait observé.
La visualisation avec le carré
Jules a visualisé le produit x × y comme une opération sur des carrés :
┌─────────────────┐
│ │
│ Carré de │ Aire = (S/2)²
│ côté S/2 │
│ │
└─────────────────┘
Le produit (S/2 + d)(S/2 – d) correspond à l'aire du grand carré moins un petit carré de côté d :
Produit = (S/2)² - d²
C'est l'identité remarquable (a+b)(a-b) = a² – b², qu'il a retrouvée intuitivement.
Déduction de la formule
Puisque P = (S/2)² – d², on isole d :
d² = S²/4 - P
d = √(S²/4 - P)
D'où la formule finale :
x = S/2 + √(S²/4 - P)
y = S/2 - √(S²/4 - P)
Vérification formelle avec Lean 4
Pour m'assurer que le raisonnement de Jules était mathématiquement rigoureux, j'ai décidé d'utiliser Lean 4, un langage de programmation conçu pour écrire des preuves mathématiques vérifiées par ordinateur.
Qu'est-ce que Lean ?
Lean est un assistant de preuve : un langage de programmation où l'on écrit des théorèmes et leurs démonstrations. Le compilateur vérifie automatiquement que chaque étape de la preuve est logiquement correcte. Si le code compile, la preuve est mathématiquement valide.
Installation de Lean 4
J'ai installé Lean 4 en quelques commandes :
# 1. Installer elan (gestionnaire de versions Lean)
brew install elan-init
# 2. Installer Lean 4 stable
elan default stable
# 3. Créer un nouveau projet avec Mathlib
lake new theoremes_jules
cd theoremes_jules
# 4. Ajouter Mathlib comme dépendance (dans lakefile.toml)
# puis télécharger les dépendances
lake update
Le code Lean pas à pas
Voici la formalisation complète du théorème de Jules, avec des explications pour chaque partie :
import Mathlib.Data.Real.Sqrt
Import : On importe le module de Mathlib qui contient la définition de la racine carrée sur les nombres réels (Real.sqrt) et le lemme Real.sq_sqrt qui dit que (√z)² = z.
def EstSolutionSommeProduit (x y S P : ℝ) : Prop :=
x + y = S ∧ x * y = P
Définition : On définit ce que signifie “x et y sont solutions du problème somme-produit”. C'est une proposition (Prop) qui est vraie si et seulement si :
– x + y = S (la somme vaut S)
– ET (∧)
– x * y = P (le produit vaut P)
theorem formule_jules (S P : ℝ) (h : S^2 / 4 - P ≥ 0) :
EstSolutionSommeProduit
(S / 2 + Real.sqrt (S^2 / 4 - P))
(S / 2 - Real.sqrt (S^2 / 4 - P))
S P := by
Énoncé du théorème :
– S P : ℝ — S et P sont des nombres réels
– h : S^2 / 4 - P ≥ 0 — on suppose que S²/4 – P ≥ 0 (sinon la racine carrée n'existe pas dans ℝ)
– Les deux arguments suivants sont x et y selon la formule de Jules
– EstSolutionSommeProduit ... S P — on veut prouver que x et y sont bien solutions
– by — on commence la preuve en mode tactique
constructor
Tactique constructor : Comme on doit prouver une conjonction (A ∧ B), cette tactique sépare le but en deux sous-buts :
1. Prouver que x + y = S
2. Prouver que x * y = P
· ring
Première partie (prouver x + y = S) :
– ring — résout automatiquement l'égalité algébrique
En effet : (S/2 + √...) + (S/2 - √...) = S/2 + S/2 = S ✓
· have h1 : (S / 2 + Real.sqrt (S^2 / 4 - P)) * (S / 2 - Real.sqrt (S^2 / 4 - P))
= (S / 2)^2 - (Real.sqrt (S^2 / 4 - P))^2 := by ring
rw [h1, Real.sq_sqrt h]
ring
Deuxième partie (prouver x × y = P) :
– have h1 : ... := by ring — on établit un fait intermédiaire : le produit (a+b)(a-b) = a² – b² (identité remarquable), prouvé par ring
– rw [h1, Real.sq_sqrt h] — on réécrit en utilisant h1, puis on applique le lemme Real.sq_sqrt qui dit que (√z)² = z quand z ≥ 0 (ce qu'on sait grâce à l'hypothèse h)
– ring — on conclut que (S/2)² – (S²/4 – P) = S²/4 – S²/4 + P = P
Le verdict
✓ Build successful
Le code compile — donc la preuve est mathématiquement correcte. Le théorème de Jules est formellement vérifié : sa formule donne bien deux nombres dont la somme est S et le produit est P.
Contexte historique
François Viète (1540-1603)
Jules a redécouvert ce qu'on appelle les relations de Viète, du nom du mathématicien français François Viète.
En 1591, Viète publie In artem analyticem isagoge, un ouvrage qui fonde l'algèbre moderne. Il est le premier à utiliser des lettres pour désigner les inconnues (voyelles A, E, I...) et les constantes (consonnes B, C, D...). On lui doit l'invention du calcul littéral.
Les formules de Viète établissent que pour un polynôme du second degré x² – Sx + P = 0 : – La somme des racines = S – Le produit des racines = P
C'est exactement le problème solutionné par mon fils.
Le lien précis avec la formule de Jules
Jules a résolu le problème inverse de Viète : connaissant S et P, retrouver x et y.
Si x et y vérifient x + y = S et x × y = P, alors x et y sont les racines du polynôme :
t² - St + P = 0
La formule quadratique classique donne :
t = (S ± √(S² - 4P)) / 2
En réécrivant cette formule :
t = S/2 ± √(S² - 4P)/2
t = S/2 ± √((S² - 4P)/4)
t = S/2 ± √(S²/4 - P) ← C'est la formule de Jules !
| Viète (1591) | Jules (2024) |
|---|---|
| Si x, y sont racines de t² – St + P = 0 | Connaissant S et P |
| Alors x + y = S et xy = P | Trouver x = S/2 + √(S²/4 – P) |
| (sens direct) | (sens réciproque) |
Mon fils a donc retrouvé la formule quadratique par un raisonnement purement géométrique, ce qui est exactement dans l'esprit des travaux de Viète — établir le lien entre les racines d'un polynôme et ses coefficients.
Sources : – Formules de Viète – Math93 – François Viète – CultureMath (ENS) – Biographie de Viète – Bibmath
Les mathématiciens grecs et l'algèbre géométrique
L'approche de Jules — raisonner avec des carrés et des aires — rappelle celle des mathématiciens grecs anciens.
Le Livre II des Éléments d'Euclide (vers 300 av. J.-C.) contient ce qu'on appelle l'algèbre géométrique. Euclide y démontre les identités remarquables par des constructions de carrés et de rectangles, exactement comme Jules l'a fait intuitivement.
Par exemple, la proposition 4 du Livre II énonce que « le carré de la droite entière est égal aux carrés des segments, et à deux fois le rectangle contenu sous les deux segments » — c'est notre identité (a+b)² = a² + 2ab + b².
Cette tradition géométrique a influencé les mathématiciens arabes comme Al-Khwarizmi (VIIIe siècle), dont le traité Abrégé du calcul par la restauration et la comparaison utilise les identités remarquables d'Euclide pour résoudre les équations du second degré.
Sources : – Livre II des Éléments d'Euclide – Wikipédia – Identité remarquable – Wikipédia – Les identités remarquables – Automaths
Conclusion
À 15 ans, Jules a redécouvert de manière autonome un résultat fondamental de l'algèbre, en utilisant une intuition géométrique remarquable. Son approche — décomposer deux nombres symétriquement autour de leur moyenne — est élégante et montre une compréhension profonde de la structure mathématique.
Ce qui me frappe, c'est que son raisonnement suit exactement la tradition des mathématiciens grecs : penser l'algèbre géométriquement, avec des carrés et des aires. Sans le savoir, il a refait le chemin d'Euclide.
Grâce à Lean 4, nous avons pu vérifier formellement que sa démonstration est mathématiquement correcte. Le théorème est prouvé.