Our work titled “Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification” has been accepted to appear at the 19th Conference on Neurosymbolic Learning and Reasoning (NeSy 2025)! First author Balaji Rao, myself, and Prof Carlo Lipizzi (all from Stevens Institute of Technology!) showed how large language models can be harnessed to generate HOL/Isabelle code for theorem proving, and applied the approach to build mechanical proofs verifying the correctness of AWS access control policies.