CS 2120

This class wasn't too difficult, but I feel as though I didn't learn much about discrete mathematics, as we spent most of the semester learning how to use Lean. Professor Sullivan is a good lecturer and explains topics pretty well, so you should be fine as long as you pay attention in class and do the homework assignments.

Professor Sullivan is a really nice guy and is actually an amazing professor. He really cares about students learning and he responds to emails within minutes. He also stays up pretty late so sometimes you might get a response back even at 1 AM. However his entire curriculum is ruined by this weird proofing language called lean. It feels like I spend more time studying about lean rather than learning about discrete math. His first exam covered everything we learned from the first half and didn't deviate from it, his second exam was online and deviated a bit from his lectures but was still doable. If you want a free A, then you'll probably get it. However, it's questionable if you'll actually learn anything of substance.
#tCFF23

While there is some truth to other reviews regarding Lean being the focus of the course, I wouldn't say that as a criticism at all. There are plenty of resources available, the lecture files are very informative and well-written. With this being the only undergraduate course he teaches, it's clear that Sullivan really cares about CS. The pacing of the course was quite manageable as well, there were few homework assignments and they were quite short. Despite pop quizzes being 'threatened' semi-frequently, there was only one midterm and one final, neither was particularly difficult. #tCFF23

TLDR: I would have rather taken the class with Orrico. I think this class is an easier A, but you learn less and are annoyed by the softwares used.

Lean:
I found it annoying that my friends in the other section (Orrico) had a completely different class. They took a more standard approach whereas we got... Lean. Lean is some proofing programming language that I just don't think I'll ever use again, but more importantly, I don't think it made any of the concepts easier to understand. Although he was always very willing to help, there were frequent issues with Lean, the class container, and the github repo for most people I knew in the class. The one saving grace of Lean is that Chat GPT understands it pretty well and can help you understand if you know what to prompt.

Lectures:
He does his best to keep the lectures engaging and simplifies the concepts pretty well, but it is very easy to get distracted for a second, look back, and be lost. Also, be prepared, he WILL cold call on random students multiple times a class, and he aims for ppl in the back that are trying to hide.

Grading:
"Grades will be based on the following measures: in-class quizzes (20%); midterm and a final exam (20% each); six to eight homework assignments (40%)"
- In-class quizzes were the easiest thing ever; they serve the purpose of ensuring attendance and scare you into staying current with the content (fair enough).
- Midterms weren't that difficult, and they grade quite generously.
- Final ended up being a take-home that was very doable.
- Homeworks get more difficult as the semester progresses, but overall not terrible. Easy to get 95%+ on them all.
If you show up when you need to, do the homeworks, and put in minimal efforts studying, you should have no problem finishing with a comfortable A.

Prof. Sullivan was absolutely amazing; he really tries to connect with his students and holds frequent office hours (but they are at weird hours). Personally, the class wasn't too much of a struggle, but other classmates definitely had more trouble grasping the concepts since he uses Lean, a proof checker (which is not used by any other professors). So as long as you read the files on github you should be fine. He grades quite generously and is very kind if you go up to him for help. Overall I wouldn't really recommend the class if you had the option of the other professors. However, if you do decide to take Sullivans class, it is a lot of work, but the pay off, in my humble opinion is maybe worth it.

Professor Sullivan is an extremely knowledgeable professor and seems to genuinely care about his students. He chooses to teach discrete using lean, while not ideal, was still doable and still aided in understanding the material. Personally, whenever I approached with issues he seemed genuinely concerned and helped to the best of his ability. The Professor and the TAs graded fairly. His teaching style forces you to learn the material on your own time, but it is not as bad as everyone is making it out to be.

Update: Use his office hours if you need help. Sullivan is a very nice guy who wants his students to succeed. I went to his final exam review session and it was immensely helpful.
TLDR; Take the class with a different professor if you want to learn anything from it.
Sullivan is a very nice guy, he seems to really care about the students as people, however, he teaches the class using an obscure proofing language called Lean. There is next to no documentation available for this language and aside from his lecture examples, there are no other resources to review or read through in order to learn more about it, or even just figure out how the language works. All that he provides is the confusingly organized API. We're well over halfway through the semester at this point and we haven't done a single standard proof like all the other discrete classes are doing. I've talked to multiple people who took this class with Sullivan when it was coded as CS 2102, and they've all agreed that learning Lean made the class less about logic and proofs, and more about figuring out the syntax of a proofing language that you'll never use again. I wouldn't say that it was difficult because of the logic taught in it, that all makes complete sense and I have been able to explain why for the homework. I have just been unable to write it out in Lean.