News for hackers. Stuff that matters.
Re:Dividing a Square into 7 Similar Rectangles by martincmartin on Thursday March 09, 2023 @09:21AM (#35081420)
I agree the tools are not ready because, as you say, the foundational concepts are not yet encoded.

But for OP, the point isn't having humans understand. It's having the computer check the proof. You still use traditional journal papers for communicating the proof to humans. You're just also able to say "The proof has been verified and really is true."

Re:Dividing a Square into 7 Similar Rectangles by mkl on Thursday March 09, 2023 @06:56PM (#35088593)
Yes, but humans using the proof assistants need to be able to read and understand the proofs while they are constructing them.