U najnovijem izdanju časopisa [url=http://cacm.acm.org/]Communications of the ACM[/url] možete pročitati članak o [url=http://cacm.acm.org/magazines/2014/4/173219-formally-verified-mathematics/fulltext]formalno verificiranoj matematici[/url]. Iz uvoda:
[quote="[url=http://cacm.acm.org/magazines/2014/4/173219-formally-verified-mathematics/fulltext]Formally Verified Mathematics[/url]"]Due to developments in computer science over the past few decades, it is now possible to achieve complete formalization in practice. Working with "computational proof assistants," users are able to verify substantial mathematical theorems, constructing formal axiomatic derivations of remarkable complexity. Our goal in this article is to describe the current technology and its motivations, survey the state of the art, highlight some recent advances, and discuss prospects for the future.[/quote]
_________________
I don't know half of you half as well as I should like; and I like less than half of you half as well as you deserve.
