Automated Planning, also known as Artificial Intelligence (AI) planning is a branch of AI focused on automated decision-making and scheduling. A sub-problem within AI Planning is domain-independent planning, where we want to develop methods that are generalisable for solving planning problems in many domains. A popular modelling language for domain-independent planning is PDDL. In PDDL we model our problems as having some start state and some goal state; these states are defined by the truth-values of a set of defined predicates applied to a set of objects with corresponding types. In this work we explore the concept of dynamic macro-actions for PDDL, which are macro-actions whose utility are re-evaluated as we solve more problems, and does not require prior training. We find that dynamic macro-actions are a promising method, showing average improvements in the number of nodes explored in the search space of up to 84\% depending on the domain.

To address the challenge of the time-consuming nature of proofreading proofs, computer proof assistants—such as the Coq proof assistant—have been developed. The Univalent Mathematics project aims to formalise mathematics using the Coq proof assistant from a univalent perspective, which is based on homotopy type theory.

The Symmetry book is a textbook about symmetries in mathematics written from a univalent viewpoint. This paper focuses on formalising the proofs in chapter 3 of the Symmetry book using the UniMath Coq library. Currently, the book is partly formalised in the Agda UniMath library. In this paper, we aim to formalise the chapter using the UniMath Coq library to verify its correctness. We have successfully formalised all the theorems in sections 3.1 to 3.3, along some other minor proofs.