In this paper, we report our first experiments in using learning-assisted automated reasoning for the formal analysis of physical systems. In particular, we investigate the performance of automated proofs as compared to interactive ones done in HOL for the verification of ray and electromagnetic optics. Apart from automation, we also provide brief initial exploration of more general issues in formalization of physics, such as its presentation and foundations.
展开▼
