OK, so it’s the weekend after the second meeting… Better late than never. I was not able to make it to the second meeting, which is a shame since Saij tells me it was quite interesting! I’ll see if I can get Eric to post what he covered…

As for the first meeting, well…

It was my job to talk about , and so we gathered around and went over the pre-processing stuff, also known as the ‘preamble’ to a document. If you are interested, you can see more here. While chatting, we went into a discussion of proof-verification systems using Coq and Mizar, and their connection to . Interestingly, I have heard that Mizar is able to produce output so that one can immediately produce the typeset article (although I cannot now re-find that reference, so perhaps I am incorrect…). This led us to discuss the general inhospitality of such formal mathematics towards human readers. We then talked about the possibility of an additional program to take a verified proof from the formal setting and render it in a more human-friendly way, such as what might be required by an instructor.

Perhaps we could ‘Erdmanize’, or ‘Jiangize’ a formal text, rendering it into something either of these instructors (who ask their students to produce very different mathematical prose) would accept. Even more important, I think, would be to have the produced text include examples and perhaps counterexamples – something completely unnecessary to a formal proof checker, but very important for human understanding.

Tim is very interested in computer verifications systems, and may take us on a tour of Coq, which he is actually using in another course. Eric has already started us out on Sage, and I will be continuing the journey next week.

Speaking of which- we continued our discussion with a brief introduction to the fancy headers package (available here) and elaboration on the different environments for arranging text on the page in a ‘tabular’ form: lists, tables, arrays, et cetera. Next week, I am planning on talking about how to adjust margins and the appearance of the page, along with a better discussion of the different ‘environments’ available to us. If there is anything in particular you would like to hear about, drop a comment my way and I’ll either add it in this week, or at least have it for the future!

We finished up with a discussion of what we might cover in the future: the Haskell programming language (With a book suggested by Tim), Discrete Mathematics, Computer Proof Verification, computer modeling, SAGE, and . Tom expressed the desire, that if we do nothing else, focusing on SAGE and would be a good start for this quarter.

Thus endeth the first meeting. Hope to see you at future ones!

ex animo-

Felicis

Filed under: CAMG, Computer Science, Group Meetings, LaTeX | Leave a comment »