The goal of this project is to create a prototype system for integrating a Large Language Model with a proof-assistant, for the purpose of generating new interesting conjectures. We believe a neuro-symbolic architecture, using an LLM to generate conjectures and a symbolic theorem prover or counter-example finder to check the correctness of the generated conjectures, could be an excellent fit for the task of automatically discovering interesting and useful mathematical properties. We have recently conducted a pilot study in this area with interesting results, manually querying ChatGPT for conjectures, and now plan to further explore the strengths and weaknesses of this approach. Building a prototype system that better automates and integrates LLM-based conjecturing with a proof assistant will enable us to perform experiments systematically.