Towards a Readability Criterion for Humans and Machines
摘要
Previous research has explored criteria for evaluating the simplicity and readability of geometric proofs generated by theorem provers, primarily from a human perspective. In particular, Graziani and Quaresma examined the simplicity and readability of proofs produced by theorem provers implementing the area method, introducing geometrographic coefficients to quantify different aspects of proof complexity. Building on their work, this study extends their analysis by investigating the computational effort involved in the proof process, specifically by measuring CPU time. The objective is to determine whether, within the context of proof generation, the hypothesised human effort aligns with the machine’s measured computational workload. Given the strong connection between human effort and proof readability, this comparison may offer valuable insights for improving the readability of machine-generated proofs by considering both human cognitive constraints and computational limitations.