City Tutoring Discussion Forum

I am uncredentialed but before dropping out of my mathematics degree around a decade ago I did study some formal logic. The capstone result being the Cantor-Schröder-Bernstein theorem which states if you've got an injection from A -> B and B -> A even if A and B are infinite sets then there is a bijection.

Logic was a lot of fun and the intersection with computational mathematics was personally very interesting. I've over the years since maintained a real interest in 'formal methods' and in particular with how in contrast to Set Theory, the Calculus of Inductive Constructions or 'Type Theory' can provide an alternatively rigorous foundation for mathematical result. This is a lot like a Logic formal proof where you begin with a premises, and each following turn is like a legal move in a game, logical ANDs, ORs, IMPLIES's, CONTRADICTIONs, etc. until you reach the formally stated final result.

It has the added benefit that because there's no prose in the proof, only a list of moves, no step is ambiguous, at all, and it lends itself very neatly to a computer since each step combined is effectively a 'receipt' that the proof is valid since it was obtained by valid legal moves.

I'm curious if anyone has come across tools like Lean 4 which I'm describing above, or large collaborative mathematical projects like Mathlib4 and what your experience was like with it!

I've messed around with Rocq about a year ago, half a year ago I picked up "Type Theory and Formal Proof" by Hermann Geuvers and Rob Nederpelt (highly recommended for understanding the base CoC) and more recently I have been learning Lean 4. The primary project Ive been working on is learning category theory in order to formalize the mapping of proofs between these dependent type theories, with the end goal of making a low level dependently typed programming language.

As for my experiences with the tools, I find using them to be very helpful! Due to the direct mappings between things like logical quantifiers and implication to type theory, it's a very smooth transition if you understand how the underlying type system work. Since it's all verified by the computer it makes doing math very reassuring and has me looking forward instead of over my work to check for mistakes. One downside of the computer verification is that sometimes I find myself just trying things without actually justifying to myself whether or not it'll actually work, it's a bad habit I'm trying to get out of. I've also never worked with these proof assistants on any projects larger than a few proofs, so I cant say much about scalability.

Due to the way you speak I want to clarify a potential misunderstanding you have about the proof assistants. The "proofs" to the proof assistant aren't the list of moves (aka tactics) but rather a proof term; a "program", which has a type of the statement you are trying to prove. The tactics are simply an alternative, cleaner way to constructing proof terms (I've tried constructing them directly in Agda and Lean, the best way I've found involves spamming the transitivity of equality which in a lot of ways just feels like tactics except you have to keep track of 6 layers of parentheses lol)

I've heard great things about Rocq!

I happened upon Lean 4 as I was trying to mathematically prove properties in a C program and figured LLVM IR ought to be tight enough, or at least a sufficiently narrow subset of it could be reasoned about. I've come across the book but I've found it much too dense to make headroom into. Maybe some day but I've been trying to pick up Lean by reading Mathlib4 source and trying exercises.

I never formally studied Category Theory but it was all the rage in my Logic class and felt like the inevitable next step - would you say with a decade out of full time instruction there's a best way to pick it up again or build up to it?

Whoa cool stuff. Noob here, So what exactly is this computational way of proving things?

on a tangent, yo evening-calm, what computational mathematics you dabbled in? Some Algebraic Geometry? Algebraic Topology?

evening-calm wrote: Thu Jun 11, 2026 9:06 pm I never formally studied Category Theory but it was all the rage in my Logic class and felt like the inevitable next step - would you say with a decade out of full time instruction there's a best way to pick it up again or build up to it?

Honestly, all the books I've come across are extremely dense or on the opposite spectrum have a lot of fluff. If you're looking for a best way with a disregard for the adjacent fields (similar to the way I am), but still want a smoother experience and to grow to appreciate it more, I would recommend learning some adjacent basics about abstract algebra things first (particularly ideas of products and quotients in groups, rings and topology). There are two good books that I've come across that take opposite approaches to category theory: "Conceptual Mathematics" by Lawvere takes a much slower approach with a lot of examples and real life applications (including about discrete systems which map to a lot of programming concepts), so I think in a lot of ways it's more interesting but it's also way too slow for my tastes so I dropped it about a quarter of the way through. "Introducing Category Theory" by Peter Smith is a lot more dense and is the book I'm working through right now, it's pretty tough some parts but by working out the theorems on paper yourself (even with guidance from the proofs in the book) I find I'm able to get a lot from the book. Note that I haven't really studied any abstract algebras outside of category theory, so even without the afore mentioned recommended experience you will be able to make your way through the book, albeit slowly. As for lacking formal instruction, besides public schooling I'm a complete autodidact and from my experience if you have some free time and you're dedicated (both of which seem to be true) you'll be fine. You should have a bit more confidence in yourself, besides credentials the utility of schooling in modern times is that it serves as a predetermined path, it's not neccesary in that regard if you already have a path in mind.

StudentDriver wrote: Thu Jun 11, 2026 11:38 pm Whoa cool stuff. Noob here, So what exactly is this computational way of proving things?

There are two major components to the proof assistants, the proof checking and the automation. The proof checking is simply that the computer can tell whether a proof actually proves a statement or if it doesnt, so any statement proved within a proof assistant can be considered to be true (that is, if you trust the kernel of the proof assistant). This serves to eliminate human error in more linguistic proofs.

The proof automation is just as it sounds, it serves to automate tedious parts of proofs. For example, Lean4 can automatically prove that a given solution to a linear system of equalities is in fact a solution so you dont have to work through the tedious aspects that formal proof entails, such as manipulating statements with associativity and commutativity (which can't be taken for granted in these systems).

evening-calm wrote: Thu Jun 11, 2026 9:06 pm I never formally studied Category Theory but it was all the rage in my Logic class and felt like the inevitable next step - would you say with a decade out of full time instruction there's a best way to pick it up again or build up to it?

One of the difficulties I had learning category theory was that it felt very unmotivated until I learned more fields of mathematics and adjusted my expectations for what it was designed to do. One of it's main uses within pure mathematics is providing common ("categorical") definitions for various types of objects across many fields of math; it shows you how many things you know all actually instances of a higher pattern. The problem is, if you don't know many interesting categories, then you won't have many examples for these very abstract definitions. This is what made it so difficult for me to learn when I was new to math. It's not so easy to appreciate a concept like adjoint functors if you only have two examples, or if you only have a working knowledge of a few categories.

Anyway, I mentored a very bright undergrad in category theory and functional programming recently. We used Awodey's book for category theory. Awodey includes many examples from logic and computer science, something that books focused more on pure mathematics don't. He technically doesn't assume much background, but it will probably be easier if you know some basic algebraic structures like groups and monoids. You could give it a shot!

@StudentDriver Mostly Lean 4 theorem proving of late, though previously I had a really strong interest in video games and while making my own or mods for games I liked the physics engines were of particular note.

This was a main gripe. I enjoy programming as a hobby but I don't want to do a lot of it, I was always much more interested in the maths. So when you're modding a game you end up in a situation where the physics you want to do is quite constrained by your ability to create algorithms and data structures to facilitate this.

Now - that can be fun too, and there's a deep mathematics in Complexity Theory which I enjoy as well, but at least until recent advances in AI coding agents, there's just a lot of fatigue and grind to make anything work.

Mathematics software packages like Maple, Mathematica, or MATLAB have high promises of getting out of the engineers/physicists/mathematicians way but in practice outside of a few neat demos there's nothing much there. If anything, it justifies the programming grind more since I'd rather go through the grind and get something good then skip the grind for something quite inferior in result just to feel superior that I could feel less of a programmer and more of a <whatever discipline is yours here>.

@MagiOmni Cheers for the book recommendations, I will check them out when I can!