From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/4626 Path: news.gmane.org!not-for-mail From: Jacques Carette Newsgroups: gmane.science.mathematics.categories Subject: Re: Bourbaki and Categories Date: Mon, 22 Sep 2008 17:09:24 -0400 Message-ID: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241020065 14095 80.91.229.2 (29 Apr 2009 15:47:45 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:47:45 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Mon Sep 22 20:36:52 2008 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 22 Sep 2008 20:36:52 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Khuq5-0004X8-Ic for categories-list@mta.ca; Mon, 22 Sep 2008 20:29:09 -0300 Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 122 Original-Lines: 82 Xref: news.gmane.org gmane.science.mathematics.categories:4626 Archived-At: I hereby volunteer my time and the technical resources I have at my disposal to 'host' a "New Bourbaki based on CT" project. Why me? 1. I am an interested _user_ of category theory, but not an 'inventor' in the field. Neutrality is frequently an asset in a "keeper of the infrastructure". 2. I need the results of such a project! My core work (for 11 years in industry and now 6 in academia) is in "mechanized mathematics", or computer-based tools that help automate the mathematics process, explicitly including both computation (i.e. what Maple does) and proof (i.e. what Coq does). (The curious can see http://imps.mcmaster.ca/mathscheme/publications.html for some of our work and my personal publications page for more). One cannot simultaneously build a library of mathematics and know category theory without seeing its tendrils everywhere. 3. I have a real stake in seeing "mathematics on computers": not only is it my day-to-day research, I am also the Chair of the Electronic Services Committee for the Canadian Mathematical Society (CMS). I am actively searching for *good* applications of "electronic services" where we can get involved. I cannot promise the resources of the CMS for this, but I can certainly promise to bring this up as an agenda item for our December meeting in Ottawa. However, I would be extremely proud if I could claim, years from now, that "Bourwiki" was a ``truly international project which benefited from a strong involvement of the Canadian Mathematical Society''. Jacques Carette PS: Below here are some minor comments/thoughts on the various topics in this email thread -- the only important parts are above. 1. I am fairly fond of the (awfully titled) book "Post-modern Algebra" http://www.amazon.com/Post-Modern-Algebra-Applied-Mathematics-Wiley-Interscience/dp/0471127388 by J. Smith and A. Romanwska, as a middle-ground between full-fledged use of categories and classical algebra in an introductory text. The organization of the text is definitely non-classical and tries to organize concepts according to mathematical criteria rather than historical timelines. 2. I definitely believe that a proper encoding of modern mathematics into a 'library' should be done top-done by specializing abstract concepts. The "Little Theories" method from theorem proving is essentially the recognition that a large body of mathematics is a huge diagram in an appropriate category of theories. These issues are all too frequently treated as meta-mathematical. The constructive theory of "representations of theories" (via sketches or otherwise) can play a very important role in software construction. 3. Heuristics and examples are crucial for human understanding of mathematics. Thus, while a "mechanized mathematics system" may be built from highly abstract pieces, it needs to present itself to its users in as concrete a manner as possible. This dichotomy between system-building and usability is further explored in a paper "High-Level Theories" (available officially at http://www.springerlink.com/content/b1122523vtm88w73/, unofficially at http://imps.mcmaster.ca/doc/hlt.pdf ) 4. I cannot over-emphasize my agreement with Joyal's statement that "But mathematics is naturally organised and simple!" 5. To a certain degree, some libraries (like those of the large theorem provers) attempt "partially unified presentations of mathematics"; some even have pseudo-databases. These are unfortunately quite classical in their structure, with the exception of the work of the Kestrel Institute (in computer science) which is very categorical. The algebra library of the programming language 'Aldor' (www.aldor.org) was definitely influenced by categories. Category theory is actively influencing the development of the language 'Haskell'. 6. What I propose to help with are the technical and online aspects of Andre Joyal's proposal: > A special database for mathematics should be created > (but I dont know how). > Papers in the NB section of the arXves could be selected, > modified and organised with a system of references, > to give a partially unified presentation of mathematics. > The same database could support different > presentations realised by different competing teams. > Each team could work like a mathematical journal, > with an editor in chief and an editorial board. > using means like the ones which Andrej Bauer suggested.