theorem proving

Theorem proving systems help produce or verify mathemantical proofs. AI may be used to aid a human mathematician or to completely automate the proof. If the proof is expressed in a suitably formal system (e.g. Lean) dedicated and trusted algorithms can be used to verify the proof. AI is used in two main ways: (i) as heuristics to suggest good paths for a proof to proceed, for example generating intermediate lemmas; and (ii) to translate human language expressions of a problem into formal representations, in particular using LLMs. The first of these is relatively safe, the latter still needs a human to check that it really is representing the intended meaning – this is the formality gap.