Hi Bill, | The first thing I did with your Mizar code was to remove them. | | Wow, you were really working, I feel guilty. The file joe.miz has the | fancy character turned into Mizar, for, ex, st, implies, etc.
Thanks! Yes, it was actually more work doing that than porting the first few ASCII-fied proofs to miz3, which is some sort of tribute to Freek. | | It sure makes the code more readable. | | That's a matter of opinion. | | It's definitely my opinion, and I know when I came to it. I was | staring at my proof of Gupta's theorem and I said to myself, I can't | read this, I have no idea what I'm writing. After I wrote my Emacs | code and stuck in (the top-level bits?) =E2=87=92, =C2=AC, =E2=88=A8, =E2=88=A7, =E2=89=A1, =E2=88=80, =E2=88=83 and =E2=87=94, it | was so much more readable. That's the way mathematicians actually | write, of course, so it's hard for me to read anything else. Obviously the full range of mathematical notation can make things much easier to read, but personally I can't get very excited about the use or non-use of a few special characters. I find that I rapidly reach the stage where I map between them without thinking, and sometimes the use of special characters instead of combinations of traditional ones makes things needlessly obscure to outsiders. Anyway I am quite surprised and a little shocked to find a Scheme programmer caring about concrete syntax :-) | I would discourage it and advise you to set up some additional | interface layer. | | I'll do it your way, you're the expert. What do you mean? Something | like my Emacs stunt to rewrite the file before compiling it? Is there | a clean way to do that? I wasn't too happy with my solution. I'm certainly not the expert on this topic, but yes something like your existing emacs tricks seem reasonable. Anway it's one of those problems that is obviously trivial, though not necessarily easy. | 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. Yes, this is one of the very appealing things about formalization, that the question of the correctness of a proof becomes an objective one. | The middle school math coordinator where I live told me to read an | article by an education prof Stylianides | The Notion of Proof in the Context of Elementary School Mathematics | who claimed that a 3rd grade girl Betsy failed to give a proof that | odd + odd = even, on the grounds that the other 3rd graders didn't buy | her proof. Betsy's proof was fine, and the objections were silly (you | can't even say all the numbers!). If Betsy has a` good proof | assistant to code her proof in, these PoMo objections disappear. That's not good, indeed. Thanks for the pointer --- I found the paper online and I'll be interested to see the details. John. ------------------------------------------------------------------------------ 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
