Limitations

LeanDojo has the following limitations. Addressing them won’t be our priority in the near future, but we welcome contributions:

• LeanDojo cannot extract data from the lean4 repo itself nor interact with theorems in it.

• Currently, LeanDojo cannot process Lean repos that use FFI, e.g., [LeanCopilot](https://github.com/lean-dojo/LeanCopilot).

• LeanDojo does not support term-based proofs or proofs that mix tactics and terms.

• Theorems extracted by LeanDojo are “syntactic theorems”, i.e., they are Lean constants defined using keywords theorem or lemma. First, they are not guaranteed to be real theorems (Lean constants of type Prop). Second, theorems defined in other ways (e.g., using def) are not extracted.