Le formalisme en mathématique

[jaber ben hayen]

bonjour

depuis le début du siécle beaucoup de sscience se sont retrouvé a lier a l informatique d une maniére ou d une autre, mais les math ont longtemps résisté a cet démarche formelle, de nos jours beaucoup de problémes de math ont pue etre modéliser en informtique tel que les suite numérique, les EDP et autre
Ma question ou mon débat porte sur la possibilité de tout formaliser en math, de tout décrire par un programe informatique, notament les probléme trés théorique qui touche au mathématique fandamentale tel qu un probléme qui pourais se poser en cours d analyse fonctionelle ou de topologie, ou ce qui est lier a la nature des espace comme les espaces d hilbert ou de soboleve ou par exemple l application du théoréme d inversion local.

bref est ce qu on peut tout formaliser en mathématiques et merci pour votre participation

[khivapia]

Bonsoir

Il y a un théorème qui dit qu'il y a un isomorphisme entre les démonstrations mathématiques et les algorithmes informatiques ! (Curry-Howard, cf http://fr.wikipedia.org/wiki/Isomorphisme_de_Curry-Howard )

A suivre...

[Anonyme]

lu all

effectivement c un probleme tres interessant, et si un tel programme existait, il pourrai servir de support de raisonnement des mathematiciens ki l utiliseraient.

Un tel programme servirait egalement de base de donnee de la connaissance mathematique, parce que pour k un theoreme soit vrai a son sens, il aurait besoin de se referer a tous les theoremes qu il utilise pour sa demonstration... et ainsi de suite jusqu aux axiomes de la theorie dans laquelle il vit.

Donc notion primordiale d alphabet, de language, de logique.

Le probleme des metamathematiques se pose, celui de transfert de verité:
comment la veracite des notions utilisées se transfert t elle d une ligne a la suivante dans une demonstration?
Un tel programme, s il ne sait le faire lui meme, doit stocker pour chaque ligne d une demonstration une valeur de verité que lui attribue le mathematicien (ou la communauté mathemetique) qui le redige.

Pour finir ce preambule, car je pense que je reviendrai sur ton topic avec des references a vous citer, un de mes profs m a dit un jour que ce qui ete utile (et interessant ?) chez un etre mathematique, c est ses proprietes, bien plus que sa definition...
a++

[Anonyme]

au fait, faudrait ke je m inscrive non?

[Anonyme]

le theoreme de godel, vous connaissez ?. Il interdit que la totalité des maths soient "demontrables" : il est des choses que l'on ne peut demontrer, donc qui ne pourront pas être mise en informatique...

[Anonyme]

yep on connais mais c pas sa k on demande de faire a un tel programme
ni a u mathematicien d ailleurs!!
on va pas chercher a demontrer quelque chose d indémontrable, lol