> Of course Lean proofs are rarely a good way to understand proofs, but hopefully they can be used to generate more human understandable arguments.
I would object to the first part: Of course there is a nontrivial learning curve, but then I'd argue that non-slop Lean/Agda/Rocq/... formalizations are amazing for understanding proofs. A good formalization presents the outline and the key arguments in nicely structured form, and then, unlike pen-and-paper proofs, also allow you to get the details on every single step, exactly to your desired level of depth.
The proofs in Martín Escardó's TypeTopology Agda repository come immediately to my mind as an example. [An interactive Agda tutorial is here: lets-play-agda.quasicoherent.io]
In contrast, LLM-generated formalizations can currently be extremely messy. They certify truth and can also contain interesting arguments, but substantial work is required to bring them into a shape that contributes to the actual goal of improving our understanding of the mathematical landscape.
Strongly depends on the subbubble of mathematics. In some parts of type theory / formal proofs for instance, there is a rather strong rejection of LLMs (for moral reasons in addition to quality reasons). The proof assistant Agda was even forked for this reason: https://types.pl/@amy/116522250630340534
> If I defined some pointless construction and it turned out to be very difficult to prove, it would absolutely and automatically over time be considered a "high utility" problem (again, for some odd reason).
Yes and no.
No: There are lots of very hard open problems which are judged to be of little value by mathematicians and hence garner little attention.
Yes: If a conjecture resists proof for a long time, this can indicate that we still have a substantial gap in our understanding. We project utility into an eventual closure of this gap, not into the statement of the concrete conjecture at hand. The gain in understanding is what we actually work for. It just turns out that chasing specific results, even if they are mostly dead ends on their own, is useful for orientation.
The (by now solved) problem by Fermat (for all integers a ≥ 1, b ≥ 1, c ≥ 1, n ≥ 3, the equation aⁿ + bⁿ = cⁿ does not hold) and the (still open) Collatz conjecture are perhaps good illustrations of this situation.
> Can I ask one question? Why not use hibernation at that point?
The sibling post by cyphar gives a good reason; while UEFI Secure Boot has its own share of issues, it can be a valuable ingredient in defending against evil maid attacks.
But another reason is... convenience. Resuming from RAM is faster than resuming from disk, especially so if your "disk" is actually just a USB flash drive. I know that it might be a bit weird to ask for convenience when the motivation is security. But I argue that there are use cases where the tradeoff is sound.
With hibernation, all your data is safe but the inconvenience might seduce you not to use it.
With suspend to RAM and your distro's version of cryptsetup-suspend (and the kernel patch or alternatively the cryptsetup workaround), only your volume key (and hence the bulk of your data, potentially terabytes worth of sensitive information) is safe, but sensitive data in memory (recent files, recent chat messages, session cookies, ...) is not. But on the other hand it's quick.
Some people use a combination: suspend to RAM for short breaks, where they expect to remain physically able to fully switch off the laptop when something happens; and suspend to disk for longer breaks.
No, it is indeed a kernel bug in the code path responsible for luksOpen.
Debian (and the distributions which ported cryptsetup-suspend) relied on cryptsetup luksSuspend doing its thing correctly, and cryptsetup luksSuspend relied on cryptsetup luksOpen doing its thing correctly, and cryptsetup luksOpen relied on the thread keyring being purged from memory on process exit, which is promised in the tread-keyring(7) manpage.
Yes, you are right: LUKS encryption protests your data at rest. An attacker which steals your disk can only gain little, like the information that you have used LUKS (unless you put your LUKS headers elsewhere, separated from the disk) and perhaps disk and disk sector usage statistics.
Sorry, aimed for a technically precise title and didn't want to bait clicks.
Yes, this does not affect people on stock configurations for the plain reason that they wouldn't expect the volume key to be safe during suspend anyway.
Debian's solution was ported to several (most?) other distributions and I guess quite a few people maintained private ports.
The thread-keyring(7) manpage promises: "A thread keyring is destroyed when the thread that refers to it terminates." For their key upload (from userspace to kernelspace) mechanism, the cryptsetup project relied on this property; but kernel 6.9 introduced a regression invalidating this property.
Several options. One is you restart and boot from a live system where you are root, and then dump all memory. This is described in the paper with the witty title "Lest We Remember: Cold Boot Attacks on Encryption Keys":
Other options: DMA attacks. Also you never know what the Intel Management Engine hidden in your computer is doing. It's running a version of Minix you don't have any control over, and it has full access to memory.
Exactly. Cryptsetup wouldn't know about the extra copy of the volume key in kernel memory. Which is why, dramatically, it appeared secure ("surely I wouldn't be asked to resupply the passphrase if the volume key is still in memory, right?").
Qubes OS, the Linux distribution aspiring to offer a reasonably secure operating system, pioneering a "every app runs in a virtual machine" approach in the Linux laptop/desktop space, tracks this at the following issue:
Suspend to (encrypted) swap might be a good middle ground between you and grandparent. Suspend to memory will (at best) protect your LUKS volume key, but other sensitive data remains.
A couple of years ago, three security researchers from the TU Munich implemented a prototype for also encrypting (most) parts of the memory just before suspend, to address this limitation; but as far as I know, it was not upstreamed or developed further: https://www.sec.in.tum.de/i20/publications/fridgelock-preven...
Yes, if you simply suspend your laptop on most stock Linux distributions, then everything including the master key is still kept in memory. But Debian pioneered the (optional) cryptsetup-suspend addon. This issues a luksSuspend command which is supposed to wipe the key from memory, and on resume asks you to resupply your passphrase.
Up to kernel 6.8, this worked as described; starting with kernel 6.9, it silently didn't.
It is a configuration language with general programming features, but it is decidedly _not_ Turing complete. It seems to sit at a sweet spot between "just JSON, no programming convenience at all" and "full-blown programming language with nontrivial toolchain".
Just a tiny addition: Yes, N log N is the average time, but the distribution is heavily long-tailed, the variance is quite high, so in many instances it might take quite some time till every item has been visited (in contrast to merely most items).
The keyword to look up more details is "coupon collector's problem".
A good friend of mine was recently sentenced to prison for publicly using this kind of phrase during a protest for climate justice. When Germany's equivalent of the Supreme Court, the Bundesverfassungsgericht, learned of this case, the court immediately ordered their release and declared the original verdict void: According to the Bundesverfassungsgericht, (in the specific situation at hand) this phrase is more a value judgment and less a factual claim.
Together with a fellow activist, who also served as informal legal counsel, they gave a talk on this case at the 38th Chaos Communication Congress: https://www.youtube.com/watch?v=r5RmTOGucZo
I would object to the first part: Of course there is a nontrivial learning curve, but then I'd argue that non-slop Lean/Agda/Rocq/... formalizations are amazing for understanding proofs. A good formalization presents the outline and the key arguments in nicely structured form, and then, unlike pen-and-paper proofs, also allow you to get the details on every single step, exactly to your desired level of depth.
The proofs in Martín Escardó's TypeTopology Agda repository come immediately to my mind as an example. [An interactive Agda tutorial is here: lets-play-agda.quasicoherent.io]
In contrast, LLM-generated formalizations can currently be extremely messy. They certify truth and can also contain interesting arguments, but substantial work is required to bring them into a shape that contributes to the actual goal of improving our understanding of the mathematical landscape.