• ## Pages

 bob on Proof that Humans Are Evi… Mike on Viking Metal Meets Viking… sir on Set Algebra: A Quick Reference… Crystal on Proof that Humans Are Evi… Felicis on Viking Metal Meets Viking…

## And Speaking of Biologists and Mathematics

Well, I see that Nick has been a little more active this last month.  Thus, it is with great guilt that I try to step beyond my laziness and post something!

First, some announcements:

• I am going to try keeping the Mathematical Biology Seminar going this Fall quarter, though the meetings will be every other week.  My plan is to focus on Neural Network modelling and the use of NEURON software to implement some simple network models.
• I would also like to keep the old CAMG meeting going, assuming there is any interest.  Drop a comment is you’d like to join us in exploring $\LaTeX$, as well as some other software.

## CAMG: First Meeting Notes

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 $\LaTeX$, 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 $\LaTeX$. Interestingly, I have heard that Mizar is able to produce $\LaTeX$ 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 $\LaTeX$ journey next week.

Speaking of which- we continued our $\LaTeX$ 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 $\LaTeX$. Tom expressed the desire, that if we do nothing else, focusing on SAGE and $\LaTeX$ would be a good start for this quarter.

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

ex animo-

Felicis