aureianimus

5 ms·

1.
by aureianimus 5d ago
The thing is that there is a standard format where the definition of the theorem is split from the proof, and verifying that the definition matches the mathematical concept is a LOT less work then reading the proof, especially if you'r
2.
by aureianimus 12d ago
There's no guarantee that the intermediate statements match the informal mathematical intermediate statements, but if there is a mismatch, then this has to be repaired elsewhere to yield a proof that passes the Comparator tool. Running
3.
by aureianimus 2mo ago
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, rather than "not making mistakes". I think it
4.
by aureianimus 2mo ago
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 or stressing particular parts with intonation is a big deal
5.
by aureianimus 2mo ago
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.com/leanprover/comparator ) This e
6.
by aureianimus 2mo ago
Graphlib? Do you have a link to this for me?
7.
by aureianimus 8mo ago
I have this with my phone, but it's because of dust. Did you try cleaning the port?
8.
by aureianimus 10mo ago
With respect to Lean/Rocq, that's true, with the subtle difference that Rocq universes are cumulative and Lean's are not.
9.
by aureianimus 11mo ago
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 who's self-worth seems to be tied to putting their mark
10.
by aureianimus 11mo ago
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, just to get a feeling. If you are serio
11.
by aureianimus 11mo ago
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 the default axioms. This causes Lean to lose subject reducti
12.
by aureianimus 11mo ago
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 hypothesis. Another pitfall is defining some object, but me
13.
by aureianimus 2y ago
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?)
14.
by aureianimus 3y ago
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 Syncany and said internship helped me indirectly land the ro
15.
by aureianimus 3y ago
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 will compile, which certifies correctness to so
16.
What if we could verify NPM packages?(hackernoon.com)
2 points by aureianimus 7y ago|0 comments