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.