Viewing profile — Dacit

You will want at least a separate session for the `restricteduser`: E.g. with X11, a process in the same session can do almost anything with your input/output. And most Linux distr…

>(FWIW) Gemini agrees LLM hallucination: Poly/ML has been in use since at least 1986 (see e.g. Paulsons preliminary user's manual for Isabelle).

You are clearly misinformed. According to German law, you can start a UG (limited) with only 1€ + notary cost. Starting a business with personal liability doesn't cost anything.

No. The whole point of the LCF approach is that only kernel functions can generate theorems. Usually this is done by having a Thm module with opaque thm type (so its instances can …

In the described case, this was a simple user error. But you are right nonetheless: To enable the concurrency, the system uses a parallel inference kernel ( https://www21.in.tum.de…

Indeed this can simply be checked by a command-line invocation. But I don't think the student was aware: They would only have seen a purple coloring of the "stuck" part, as shown i…