You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Patrick Nicodemus (Dec 06 2021 at 15:20):The year is 2021. Computers are everywhere. Intuitively it seems like we must be able to use computers to make mathematical research easier, if only in small ways. Besides LaTeX, youtube, teleconferencing and email, how do you use a computer to assist in your research? Do you use a proof assistant like Lean or Coq or NuPRL? Do you use computer algebra systems like Sage or Macaulay2?
If you were talking to someone who was working on similar problems to you, what computational tools would you recommend that they become familiar with? How have you used them to help you with problems? What can you do with a computer that can't be done on pencil and paper?
Morgan Rogers (he/him) (Dec 06 2021 at 15:45):Patrick Nicodemus said:
Besides LaTeX, youtube, teleconferencing and email...
This Zulip is certainly on my list, plus overleaf/github for collaborative writing, and whatsapp/other messaging systems for faster-than-email communications, not to mention all of the online resources that I need on a day-to-day basis. For me, that's it, although my collaborator @Jens Hemelaer has done enough programming to help us compute some (counter)examples of exponential objects in presheaf toposes.
Mike Shulman (Dec 06 2021 at 15:48):Do you use a proof assistant like Lean or Coq or NuPRL?
Yes. In particular, when working in exotic foundational systems and internal languages, interactive tools like this can be invaluable to aid in developing intuition, in addition to simply verifying correctness.
Henri Tuhola (Dec 06 2021 at 15:49):I'm in middle of learning agda. My main motivation is in writing software that no longer crashes.
Matteo Capucci (he/him) (Dec 06 2021 at 21:26):q.uiver.app is my best friend lately
Matteo Capucci (he/him) (Dec 06 2021 at 21:28):I'd love to use proof assistants more but most of the things I do would require more assistance from me to the computer than viceversa. I still believe in the long run I would benefit more than not from doing it, but the activation energy is too high to overcome my laziness.
Daniel Geisler (Dec 07 2021 at 01:10):My professional background was as a programmer in large part because I needed the mastery of computers to do my research in dynamics.
tetration period
Since I had no one to check my work I began using computers to do so. For example I derived the first thirty terms for the Taylors series of smooth dynamical systems.
http://tetration.org/Fractals/Projective/index.html
Visual proof of convergence of tetration
Jules Hedges (Dec 07 2021 at 10:12):Haskell was extremely integral to the birth of open games, there were a few weeks in January 2015 when I was iterating through a whole load of candidate definitions, using Haskell's type inference to quickly rule out definitions that didn't make sense, and then computing examples to rule out ones that made sense but weren't doing game theory. Later, I translated all the definitions from Haskell into mathematical prose
Fabrizio Genovese (Dec 07 2021 at 12:31):git pull, git commit -Sm "AAAAAA", git push, over and over again, forever.
Fabrizio Genovese (Dec 07 2021 at 12:31):Occasionally, I also use my computer as a punching bag to relieve stress when is particularly disappointing.
Jules Hedges (Dec 07 2021 at 12:33):In my case it's usually some variant along the lines of git commit -m "some stuff I did weeks ago and forgot to commit but I don't remember what"
Fabrizio Genovese (Dec 07 2021 at 14:15):You don't sign your commits?
John Baez (Dec 07 2021 at 14:54):Personally I only use a computer to communicate. I hate programming, but I like to work with people who like it. Steve Huntsman, Cheyne Weis and I just finished a paper where we used a lot of numerical computation to study a chaotic nonlinear PDE. For this Mathematica were MatLab was enough, but they needed some good algorithms. A much bigger project is developing compositional models of infectious diseases. Here I'm helping find good mathematical structures but Evan Patterson, James Fairbanks, Xiaoyan Li and others are writing lots of software in Julia. They call their framework AlgebraicJulia and a good place to start reading about this project is here:
Jules Hedges (Dec 07 2021 at 14:57):Generalising from what John said, many of us believe that for the majority (?) of applications of category theory, the most straightforward route between us category theorists and domain experts goes via a computer implementation of some kind
John Baez (Dec 07 2021 at 14:58):I prefer to have the domain experts between me and the computers.
Jules Hedges (Dec 07 2021 at 15:00):The pipeline goes Category theorist programmer implementation domain expert application
John Baez (Dec 07 2021 at 15:00):I didn't mention the epidemiologists on our team just now, but all of them do a lot of programming too.
Jules Hedges (Dec 07 2021 at 15:00):We don't have to talk to computers, but we definitely have to talk to people who talk to computers
John Baez (Dec 07 2021 at 15:03):For me the pipeline is nonlinear; I'm too lazy to draw it, but "category theorist" is connected to "category-knowledgeable programmers" and "domain expert programmers", who in turn are connected to "software" and to each other.
John Baez (Dec 07 2021 at 15:04):That is: I can and should talk directly to both domain experts and also programmers who know lots of category theory, and they should talk to each as they develop software.
Jules Hedges (Dec 07 2021 at 15:05):Yeah, that sounds plausible, but it was too much effort to draw a nonlinear pipeline on zulip
Nick Hu (Jan 04 2022 at 15:22):Surprised this hasn't been mentioned, but video games. I get to solve interesting problems and unwind at the same time, sometimes with friends. I undoubtedly wouldn't have pursued any kind of career in anything to do with computers if not otherwise, at least initially.