The weakest precondition of a program describes the largest set of initial states from which all terminating executions of the program satisfy a given postcondition. The generation of these weakest preconditions is an important task with practical applications in areas such as software verification and runtime error-checking. For programs containing loops, weakest precondition generation critically depends on synthesizing loop invariants that are inductive in nature; these weakest preconditions then essentially embed the inductive properties required for program verification. This paper investigates the use of Large Language Models (LLMs) to generate weakest preconditions (and accompanying loop invariants) in order to prove the correctness of non-deterministic programs containing arrays, loops, and arithmetic. Specifically, we employ several models of ChatGPT to derive the weakest preconditions and invariants for the aforementioned programs. We then compare these LLM-derived weakest preconditions and invariants to their provable counterparts obtained by the MaxPrANQ tool. We find that the quality of the LLM-derived results can vary greatly and is highly dependent on the underlying model used by ChatGPT. This variance in performance propels us to outline directions for future work and discuss how LLMs and formal-tools can complement one another in generating valid weakest preconditions and strong invariants.