Hybrid Interestingness: Fusing Contradictory Criteria from Automated Theory Formation

Research Question: Can synthesizing and reconciling conflicting interestingness measures from various domains lead to a more robust, generalizable notion of interestingness for automated mathematical discovery?

Hypothesis: Combining domain-specific and even contradictory interestingness metrics (as discussed in geometric theorem discovery and proof simplicity literature) will yield hybrid measures that outperform any single heuristic in guiding automated theory formation.

Experiment Plan: - Survey and formalize interestingness metrics from geometry, proof simplicity, and other domains (Quaresma et al., Kinyon, Pease et al.).

• Implement a meta-learning module in FERMAT that adaptively weighs and blends these metrics during exploration.
• Use multi-objective evolutionary algorithms to optimize for “hybrid interestingness.”
• Evaluate the new hybrid metric’s performance by comparing the diversity, depth, and creativity of generated theories with those generated using single metrics.
• Gather expert feedback to validate qualitative improvements in discovered theories.

References:

• Quaresma, P., Graziani, P., & Nicoletti, S. M. (2024). Considerations on Approaches and Metrics in Automated Theorem Generation/Finding in Geometry. Automated Deduction in Geometry.
• Kinyon, M. (2018). Proof simplification and automated theorem proving. Philosophical Transactions of the Royal Society A.
• Pease, A., Colton, S., & Charnley, J. (2013). Automated Theory Formation: The Next Generation.