CS 2120

I think I would have enjoyed the subject matter of this course had I not taken it with Kevin Sullivan. He teaches everything using a weird programming language called Lean. Lean is confusing and irrelevant (you will never use it for another class), and it felt like I struggle more trying to figure out the syntax of Lean instead of actually diving into the theoretical concepts so foundational to this course (and later CS ones).

The class itself wasn't super time-consuming; there were 8 homework assignments over the semester, one midterm, and one final. Some of the homework assignments were long-winded and confusing; but you are permitted to use ChatGPT and there are office hours (though at weird times). It was pretty easy to score 95-100 on all of them. The midterm wasn't too bad either; and he gave us a pretty detailed study guide that he stuck to. The final, however, was a different story. We receieved minimal details about it/no study guide, Sullivan wasn't even present during the final (a TA had to proctor) and there ended up being like 5 mistakes on it. The worst part was that the final tested us on some stuff we never went over, and expected us to know how to do things he never taught or put on the homeworks.

I think Sullivan himself is just very disorganized, which is why the second half of the semester felt like a mess. I don't think he's an effective lecturer; he tends to ramble and talk in circles. I honestly learned the content from consistently meeting with a study group during the final weeks. He does have pretty detailed lecture notes that he posts, which are decently helpful but again inconsistent with what he expects us to know how to do for tests.

If you choose (or are forced, I didn't have a choice with my schedule) to take this class with Sullivan, expect to come out of it with shaky elementary knowledge of Lean (a proofing programming language you will never use again) and a tenuous grasp of a *few* concepts in Discrete Mathematics. Because this class is so foundational to later CS courses (DMT 2, DSA 2) I would highly recommend taking it with a different professor so you might actually glean something useful from it.

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.