> This reminds me of something Andrzej Trybulec said about automated > theorem provers: why should we let the machine deprive us of the > pleasure of proving things? > > That's great, and I modified Andrzej Mizar code to write mine. , We > should use the machine to enhance the pleasure of proving things. I > get a great rush when Mizar says I have a correct proof. There's a > democracy/PoMo angle: I haven't yet talked to a grownup about Tarksi > axiom proofs, and I completely believe my proofs, because Mizar > checked them. I don't need to be part of a system that tells me I'm > right. And there's no Post Modernist talk about how proofs are social > constructs, it's up to every community to decide what a proof is.
This note from the great visionary is probably less known than it deserves to be: http://www-formal.stanford.edu/jmc/future/objectivity.html Josef ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
