Lol the other reviews are basically right. For the last month I stopped showing up to class since it only made things more confusing. The course if horribly structured, and I'm pretty sure most days Sullivan didn't actually plan out a lecture, but instead just starting making lean files and seeing if he still knew the language (spoiler alert: he didn't). But on the bright side, the TAs were all really helpful (I HIGHLY HIGHLY I CANNOT EMPHASIZE THIS ENOUGH HIGHLY recommend going to them when kevin inevitably fails you), and since everyone was super confused, this meant that there were massive curves and many bonus assignments (some of which were dropped btw??). Basically take this class with sullivan if you want to do no substantive work and also want to be massively behind in your future classes.

This class was horribly managed — Sullivan didn't even show up on the first day because he didn't know he was teaching our section. That's a forgivable mistake, but it was representative of a myriad of issues that plagued the class throughout the semester. Lectures were very obviously (or at least strongly seemed) planned poorly, with Sullivan frequently starting an example, realizing it wouldn't work, and then backtracking to use a different example that also wasn't particularly helpful. Both homework and exams were graded at an unpredictable (i.e. often late) pace, a midterm was delayed by at least a week, and in one infamous incident, a homework assignment that he announced would be uploaded within a week completely failed to materialize until days before the final exam, when it was turned into a bonus assignment (???). This doesn't even mention the fact that he requires us to use the completely obscure programming language Lean, which has precisely zero easily accessible documentation and features syntax that is incredibly non-intuitive for new users. This language sucks so bad that it's a minor victory to even have code that doesn't throw a huge amount of errors, much less actually work.
As for difficulty, in my experience I found that you either fall into one of two categories: if you have prior programming experience, it just "clicks" and the class is incredibly trivial at a conceptual level while still being frustrating to actually work on (luckily, I fell into this category). If you don't, and you don't understand what's going on, then you're shit out of luck, because going to lectures won't help you learn either. Honestly the most important skill for the class is focusing on the concepts because the tests are all open-note and heavily overlap with the homework assignments, so all you really have to do is understand what you were doing in the HW and slightly change it to match the test questions.
To be unnecessarily extra fair to the class, although Lean is still easily the worst language I have had the misfortune of dealing with, the last unit on proofs actually seemed somewhat interesting. It's just unfortunate that the overwhelming majority of the class leading up to that unit was that awful, so by then I was burnt out and didn't really bother to learn too much.

Day 1 Lecture Log:

most disorganized professor i've ever seen in my life; he literally forgot to come to the first class. He also doesn't even know what's on his homework so he accidentally goes over all the answers during class. On top of that, he never plans his lectures so every 5 minutes he gives us a "break" and writes the lesson plan during this period. I think I could teach lean better than this guy. Also who does this guy think he is: "I aim to catalyze a self-regenerative transformation of critical sectors of our society into far better performing cyber-social learning systems." Like literally 0 organisms in this world know what that means buddy.

Day 2 Lecture Log:

the beginning of today's class was fairly interesting - we went over the statistics of our recent exam. The funny part of this is that ~10 people got between a 0-7%. It was an open note exam with more than 20% of it being verbatim off the notes; this means that some people were so confused they didn't even know where to look in the notes. Side note: He came near me today and I think I almost started crying - his eyes were quite literally staring into my soul. On a more serious note, I was lost last class and it now feels like he's talking in some alien language only he understands. So, if you take this class try your hardest to understand it from the BEGINNING - maybe don't write courseforum logs in class.

Day 3 Lecture Log:

My bed is extremely soft.

\n Day 4-5:

My bed is still soft.

Sullivan is brilliant, definitely talk to him personally if you are having any issues. While he is somewhat disorganized, he teaches discreet in a much better fashion than the traditional, writing proofs with pen and paper. You are learning while the curriculum and coding languages involved are still in development - so keep that in mind. He offered many opportunities for extra credit as well. Honestly the whole class was easy if you followed along in lectures, otherwise you could catch up with his self-published materials which he offered for free.

I think the best way to describe this course and this professor is "Oh no." He is beyond disorganized and the lectures make next to no sense. This course is problematic to say the least. If possible try to take it during the summer instead because they don't use LEAN at all! Prof. Sullivan is a really nice guy and worked to accommodate for people's schedules and such, but he is like the Rising Roll of professors (that's to say that he is a hot mess). Exams are open notes and there are reviews but nothing gets graded quickly so there is very, very little feedback on your work. If you take this class, I wish you good luck...you'll need it :)

We don't learn much, but it's an easy class. But it's also easy to get totally lost and thrown off bc we use LEAN. Just take it since it's a requirement!

This class is extremely disorganized. The homework and test difficulties range from stupidly easy to ridiculously impossible. The lectures make little to no sense and sometimes he would use a tactic and never explain what it does or why he used it there. We had like 6 homeworks on the first 6-7 sections, and then like 2 on the next 12. Lectures would consistently introduce topics that we had needed for the homework that was due the night before. We didn't know the location of our final until the day before. Even the TAs were sometimes clueless as to what's going on. I doubt anyone who has ever taken this class has ever even touched Lean (the language we use to code) afterward. I could go on and on but you get the picture

Honestly, If you asked me if I learned a single thing this semester, I would say no except for how to struggle with writing proofs in lean. Sullivan is an ok professor and a very nice guy but I haven't learned anything other than how to fuck with Lean in order to try and make it work. The work is fairly easy except no one has any clue what is going on and even the TA's are confused on how to do things sometimes. I never needed to learn anything other than how to do proofs in lean, not how they work or why just that I can solve it in lean. Furthermore, a lot of the time they would give us assignments that had information we had not learned or had to use some obscure tactic in Lean in order to solve it. And this language is so obscure that when you look up "how to use and.intro in lean" it will give you results on how to drink lean......, I feel woefully underprepared going into algo and Theory.

I found this course to be extraordinarily easy, to the point where it was far too slow-moving. Sullivan teaches you all the tactics you need in lean, a fairly strange automated theorem prover that replaces the pen-and-paper aspect of this course. While I don't think you learn the logic as well as you might in a traditional discrete math course, I think lean is an interesting concept and teaches functional programming in addition to logic fairly well. The only major problem with this course is that a good amount of it has to come from self-study, which is okay as long as you find the material interesting. Sullivan commonly spends lectures showing videos of rocket crashes and telling his students that this is what can happen if your software is no good, rather than progressing the course further, making it very slow at times, since we spend more than a week on proving one type of proposition. We also never made it to sets or automata, which was disappointing, but overall one of the easier classes I've taken at UVA.

~TLDR: If you can possibly take this class somewhere besides UVA, do it. Sullivan is probably the worst professor I've ever had. He's kinda nice, but also isn't accessible and doesn't even know the material that well. ~

This is without a doubt the worst class I have ever taken. I thought that intro to engineering lab with Ann Reimers was the worst class I'd ever take but I was wrong. I at least used the information that I learned in Reimer's class, and I can't see that I will ever use this information ever again.

I came into this class excited to learn discrete math and was instead given a cheapo version of discrete in a theorem prover where the only reliable proof technique we learned was to throw commands at the theorem prover and hoping something would work. Here are some of my biggest issues with the class:
- Sullivan just used shorthand tactics while teaching instead of explaining the actual logic.
- The textbook was overly verbose and ultimately unhelpful.
- Exams frequently had material that was far harder than problems in the homework, lecture, or notes.
- Sullivan didn't hold office hours while the homework assignments were open. He posts the homework on Thursday, it’s due on Tuesday, and his office hours are on Wednesday.
- Sullivan never responds to emails.
- Sullivan doesn’t actually know lean very well, and his assignments are full of syntax errors which make it impossible to prove the theorem as written.
- Sullivan often showed up to class unprepared to teach and just made up exercises as he went which was evident by the fact that he continuously messed them up