Les limites des logiciels de calcul formel?
Dans ce billet j’ai posé l’exercice de montrer que la loi binaire
x¤y := x(y2+1)½+y(x2+1)½
définit une structure de groupe sur l’ensemble des réels. Le seul obstacle est l’associativité; la preuve n’est pas très difficile (il s’agit d’un simple transport de la loi + par le sinus hyperbolique). Mais avec Maple je n’arrive pas à faire la preuve par force brute; en effet, je ne sais pas comment faire en sorte que le logiciel simplifie l’expression concernée (tandis que le logiciel Xcas y arrive, comme l’a remarqué Tukikun).
Dans le même esprit, je me demande si quelqu’un arrive à démontrer avec Maple que, sur les courbes elliptiques (réelles), l’addition par la méthode des sécantes est associative. Je n’y suis pas arrivé.
Passe à l’algèbre de Lie du groupe ça se transforme en un bête exercice d’algèbre linéaire. En espérant que ça t’aide. Sam
J’ai une petite feuille Maple (V5) dans laquelle j’ai étudié l’associativité de la loi d’addition dans une courbe elliptique. C’est un peu artisanal, et je n’ai pas étudié le cas où 2 des 3 points sont égaux, mais en attendant quelques minutes, on obtient bien " MN_P – M_NP = [0,0] " !
Est-ce possible ici de déposer une pièce jointe ?
Bonne continuation
Oui, volontiers, cher MapleMan ! Le plus simple est que tu me envoies le fichier sur les courbes elliptiques par email à elsner{aatt}mathoman.com (j’ai Maple 11).
Entretemps j’ai vérifié l’associativité de la loi de groupe x¤y := x(y2+1)½+y(x2+1)½ avec Xcas et ça marche effectivement très bien (contrairement à Maple). En revanche je n’arrive pas à montrer analytiquement le théorème de Morley, ni avec Maple ni avec Xcas. Je t’enverrai le document Maple, peut-être tu trouveras une manière à forcer le simplification.
Mise à jour : je n’ai toujours pas reçu d’email de MapleMan. Mais entretemps j’ai réussi à prouver le théorème de Morley par Maple. En fait, comme paramètres il ne faut pas prendre deux angles du triangle, mais plutôt leurs arctangentes (la raison étant que Maple n’arrive pas à simplifier les expressions transcendantes).