Viewing profile — aureianimus

To give a more precise indication, I watched maybe the first 5 minutes of lecture 1 and 5 for this. I highly encourage you to take "didicatically useful" as a bar to aim for, rathe…

I watched some snippets, and would like to put forward some points in support of the former: - The voice is clearly TTS, which I think really loses something. Not having variation …

Very cool! It seems you've got a great setup. An addition that would be very convincing is going the extra mile and making a comparator setup for your Lean proofs. ( https://github…

Graphlib? Do you have a link to this for me?

I have this with my phone, but it's because of dust. Did you try cleaning the port?

With respect to Lean/Rocq, that's true, with the subtle difference that Rocq universes are cumulative and Lean's are not.

The version I heard involves a 3d artist adding an obnoxious fairy flying around the character, so not critical, but noticable. I also think the idea here is to apply it to bosses …

All the good resources are listed here: https://lean-lang.org/learn/ I recommend the natural number game (also mentioned above) for a casual introduction to the mathematics side, j…

I think the difference is mostly cultural. The type theories of Lean and Rocq are fairly close, with the exception that Lean operates with definitional proof irrelevance as one of …

In a lot of cases you can get far by locally proofreading the definitions. Trying to formally prove something and then failing is a common way people find out they forgot to add an…

I'd love to hear a little bit more on what you think the downsides are? (Or a recommendation for a resource to read up on this?)

Add-on story: I joined binwiederhier for a while in developing Syncany and he invited me for an internship at his current employer. The experience I gained both in contributing to …

Not strictly what you're looking for, but in Lean (functional language/theorem prover), there's some interesting work being done. Using the tool actually shows which suggestions wi…