Internetbureau Rotterdam 
Dit bericht is geplaatst op dinsdag 17 april 2007 om 09:58 in categorieën Algemeen. Je kunt de reacties volgen via een RSS 2.0 feed. Je kunt een reactie plaatsen, of een trackback van je eigen site plaatsen.
Wiskundemeisjes
Ionica & Jeanine
Formele bewijzen
In Algemeen, door wiskundemeisjes
Freek Wiedijk gaf op het Nederlands Mathematisch Congres een interessante voordracht over formele wiskunde. Tot onze verbazing maakte hij ineens reclame voor de wiskundemeisjes. Hij gebruikte het gedicht Bewijs uit het ongedichte om te laten zien hoe een formeel bewijs eruit ziet. Zie hier het resultaat.
Voor wie het plaatje te klein vindt, of meer wil weten over formele bewijzen: hier is de complete presentatie van Freek Wiedijk (pdf).
(Ionica)
dinsdag 17 april 2007 om 11:54
Ach, wat leuk. Daar heb ik nog in bemiddeld, geloof ik, zie http://www.writersblog.nl/citaten/070328-1.html -- en dan vooral de comments
dinsdag 17 april 2007 om 13:21
De volgende woorden in Wiedijks lezing vallen me wel op:
"in practice automated theorem proving is almost useless - just mindless search - computers only beat humans at ‘puzzles’ - don’t expect computers to produce interesting proofs on their own"
Bij wiskundigen die met automatische bewijsprogramma's werken zie ik vaak dezelfde afwijzende houding tegenover het volledig formaliseren van wiskunde. Zo schrijft Ursula Martin in "Computers, reasoning and mathematical practice", Computational Logic, Vol. 165 (1999), pp. 301-346 het volgende:
"The latter [full formal development of large bodies of mathematics] is at odds with mathematical practice: many mathematicians view formal proof development unsympathetically and it is hard to see it being incorporated except in expensive reworkings of well-understood material."
Ik vraag me af waaruit deze wederzijdse afwijzing voorkomt. Hebben we hier met twee verschillende 'culturen' in de wiskunde te maken? De 'formele' versus de 'pragmatische' wiskundigen?