How about these?
- rate limit overall messages, maybe even percentage wise: if some ip sent more than 70% of all messages in the last minute, mute it.
- let other users mark/report spam and if three others agree something is spam, block all slightly similar messages for 24 hours?
- forbid sending the exact same message more than N times per M seconds.
- rate limit color change and jump much more.
As Wikipedia says, "some official plugins proprietary". So "can be" is doing a lot of work in that sentence. I would at most compare it to saying that VS Code is open-source.
I think one reason for the web interface is that the device stays usable. If it would export a block device then it would need to unmount the file system on itself or at least block changes. If I remember correctly in the old days before MTP, all Android did this, making storage on the device itself unavailable while making it available via USB.
Yeah, that would be an issue with presenting the device as a block storage device.
The web interface also has a couple of other advantages: the tablet simultaneously listens for ssh connections, and can be used over Wi-Fi, IIRC? Though it could also expose a "USB HUB" with both the network interface and block storage.
I just wish we had a more ubiquitous "network file storage" protocol. The tablet itself could offer NFS, but mounting it under different operating systems would be a pain, requiring manual user intervention.
The trick is that the human only needs to read and understand the Lean statement of a theorem and agree that it (with all involved definitions) indeed represents the original mathematical statement, but not the proof. Because that the proof is indeed proving the statement is what Lean checks. We do not need to trust the LLM in any way.
So would I accept a proof made by GPT or whatever? Yes. But not a (re)definition.
The analogy for programming is that if someone manages to write a function with a certain input and output types, and the compiler accepts it, then we do know that indeed someone managed to write a function of that type. Of course we have no idea about the behaviour, but statements/theorems are types, not values :-)
The thing is, when AI systems are able to translate intuitive natural language proofs into formal Lean code, they will also be used to translate intuitive concepts into formal Lean definitions. And then we can't be sure whether those definitions actually define the concepts they are named after.
