Dear Jacques Carrette, Your wrote:
I hereby volunteer my time and the technical resources I have at my disposal to 'host' a "New Bourbaki based on CT" project.
Your offer to help is enormously appreciated. The realisation of the project depends on establishing a close collaboration between mathematicians and computer scientists. I suggest to call it iBourbaki after an idea of Valeria de Paiva. She was very helpful in answering some of my questions. Let me try to describe the problem as I see it. What is needed is an online system which can be consulted by everybody but only modified in a restricted way. The user should be able to navigate in the system by clicking on words or by doing a search. He should be able to suggest a modification or a correction. The typography is very important, it should be of the highest standard: Tex. It should be possible to draw diagrams and planar figures. The presentation of mathematics supported by the system should be the work of various teams, collaborating or competing. The system should be able to support different presentations. Let me stress that the iBourbaki project is not about theorem proving or verification. The goal is more modest: to create an interface for an efficient organisation and dissimination of mathematical knowledge (for students and researchers). The system will have to be very user-friendly, almost invisible to the user. In addition to presenting mathematics in a logical fashion, it should give informations about the applications, the history, the motivations and the heuristics. The project will have to be very practical. I am aware of the enormous difficulties of realising iBourbaki. Equally enormous will be the benefits to the community if it succeed. Andre -------- Message d'origine-------- De: cat-dist@mta.ca de la part de Jacques Carette Date: lun. 22/09/2008 17:09 À: categories@mta.ca Objet : categories: Re: Bourbaki and Categories 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-Intersci... 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. ------_=_NextPart_001_01C91D1E.004E3E13 Content-Type: text/html; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2//EN"> <HTML> <HEAD> <META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1"> <META NAME="Generator" CONTENT="MS Exchange Server version 6.5.7653.31"> <TITLE>iBourbaki</TITLE> </HEAD> <BODY> <!-- Converted from text/plain format --> <P><FONT SIZE=2>Dear Jacques Carrette,<BR> <BR> Your wrote:<BR> >I hereby volunteer my time and the technical resources I have at my<BR> >disposal to 'host' a "New Bourbaki based on CT" project.<BR> <BR> Your offer to help is enormously appreciated.<BR> The realisation of the project depends on establishing a close<BR> collaboration between mathematicians and computer scientists.<BR> I suggest to call it<BR> <BR> iBourbaki <BR> <BR> after an idea of Valeria de Paiva.<BR> She was very helpful in answering some of my questions.<BR> Let me try to describe the problem as I see it.<BR> <BR> What is needed is an online system which can be consulted by everybody<BR> but only modified in a restricted way.<BR> The user should be able to navigate in the system<BR> by clicking on words or by doing a search.<BR> He should be able to suggest a modification or a correction.<BR> The typography is very important, it should be of the highest standard: Tex.<BR> It should be possible to draw diagrams and planar figures.<BR> The presentation of mathematics supported by the system<BR> should be the work of various teams, collaborating or competing.<BR> The system should be able to support different presentations.<BR> <BR> Let me stress that the iBourbaki project is not about theorem proving or verification.<BR> The goal is more modest: to create an interface for an efficient<BR> organisation and dissimination of mathematical knowledge (for students and researchers).<BR> The system will have to be very user-friendly, almost invisible to the user.<BR> In addition to presenting mathematics in a logical fashion, it should<BR> give informations about the applications, the history, the motivations and<BR> the heuristics. The project will have to be very practical.<BR> <BR> I am aware of the enormous difficulties of realising iBourbaki.<BR> Equally enormous will be the benefits to the community if it succeed.<BR> <BR> André<BR> <BR> <BR> -------- Message d'origine--------<BR> De: cat-dist@mta.ca de la part de Jacques Carette<BR> Date: lun. 22/09/2008 17:09<BR> À: categories@mta.ca<BR> Objet : categories: Re: Bourbaki and Categories<BR> <BR> I hereby volunteer my time and the technical resources I have at my<BR> disposal to 'host' a "New Bourbaki based on CT" project.<BR> <BR> Why me?<BR> 1. I am an interested _user_ of category theory, but not an 'inventor'<BR> in the field. Neutrality is frequently an asset in a "keeper of the<BR> infrastructure".<BR> 2. I need the results of such a project! My core work (for 11 years in<BR> industry and now 6 in academia) is in "mechanized mathematics", or<BR> computer-based tools that help automate the mathematics process,<BR> explicitly including both computation (i.e. what Maple does) and proof<BR> (i.e. what Coq does). (The curious can see<BR> <A HREF="http://imps.mcmaster.ca/mathscheme/publications.html">http://imps.mcmaster.ca/mathscheme/publications.html</A> for some of our<BR> work and my personal publications page for more). One cannot<BR> simultaneously build a library of mathematics and know category theory<BR> without seeing its tendrils everywhere.<BR> 3. I have a real stake in seeing "mathematics on computers": not only is<BR> it my day-to-day research, I am also the Chair of the Electronic<BR> Services Committee for the Canadian Mathematical Society (CMS). I am<BR> actively searching for *good* applications of "electronic services"<BR> where we can get involved.<BR> <BR> I cannot promise the resources of the CMS for this, but I can certainly<BR> promise to bring this up as an agenda item for our December meeting in<BR> Ottawa. However, I would be extremely proud if I could claim, years<BR> from now, that "Bourwiki" was a ``truly international project which<BR> benefited from a strong involvement of the Canadian Mathematical Society''.<BR> <BR> Jacques Carette<BR> <BR> PS: Below here are some minor comments/thoughts on the various topics in<BR> this email thread -- the only important parts are above.<BR> 1. I am fairly fond of the (awfully titled) book "Post-modern Algebra"<BR> <BR> <A HREF="http://www.amazon.com/Post-Modern-Algebra-Applied-Mathematics-Wiley-Interscience/dp/0471127388">http://www.amazon.com/Post-Modern-Algebra-Applied-Mathematics-Wiley-Interscience/dp/0471127388</A><BR> by J. Smith and A. Romanwska, as a middle-ground between full-fledged<BR> use of categories and classical algebra in an introductory text. The<BR> organization of the text is definitely non-classical and tries to<BR> organize concepts according to mathematical criteria rather than<BR> historical timelines.<BR> 2. I definitely believe that a proper encoding of modern mathematics<BR> into a 'library' should be done top-done by specializing abstract<BR> concepts. The "Little Theories" method from theorem proving is<BR> essentially the recognition that a large body of mathematics is a huge<BR> diagram in an appropriate category of theories. These issues are all too<BR> frequently treated as meta-mathematical. The constructive theory of<BR> "representations of theories" (via sketches or otherwise) can play a<BR> very important role in software construction.<BR> 3. Heuristics and examples are crucial for human understanding of<BR> mathematics. Thus, while a "mechanized mathematics system" may be built<BR> from highly abstract pieces, it needs to present itself to its users in<BR> as concrete a manner as possible. This dichotomy between<BR> system-building and usability is further explored in a paper "High-Level<BR> Theories" (available officially at<BR> <A HREF="http://www.springerlink.com/content/b1122523vtm88w73/">http://www.springerlink.com/content/b1122523vtm88w73/</A>, unofficially at<BR> <A HREF="http://imps.mcmaster.ca/doc/hlt.pdf">http://imps.mcmaster.ca/doc/hlt.pdf</A> )<BR> 4. I cannot over-emphasize my agreement with Joyal's statement that "But<BR> mathematics is naturally organised and simple!"<BR> 5. To a certain degree, some libraries (like those of the large theorem<BR> provers) attempt "partially unified presentations of mathematics"; some<BR> even have pseudo-databases. These are unfortunately quite classical in<BR> their structure, with the exception of the work of the Kestrel Institute<BR> (in computer science) which is very categorical. The algebra library of<BR> the programming language 'Aldor' (www.aldor.org) was definitely<BR> influenced by categories. Category theory is actively influencing the<BR> development of the language 'Haskell'.<BR> 6. What I propose to help with are the technical and online aspects of<BR> Andre Joyal's proposal:<BR> > A special database for mathematics should be created<BR> > (but I dont know how).<BR> > Papers in the NB section of the arXves could be selected,<BR> > modified and organised with a system of references,<BR> > to give a partially unified presentation of mathematics.<BR> > The same database could support different<BR> > presentations realised by different competing teams.<BR> > Each team could work like a mathematical journal,<BR> > with an editor in chief and an editorial board.<BR> ><BR> using means like the ones which Andrej Bauer suggested.<BR> <BR> <BR> <BR> <BR> <BR> <BR> <BR> </FONT> </P> </BODY> </HTML> ------_=_NextPart_001_01C91D1E.004E3E13--