Comment by StilesCrisis

One real limitation is context size. 1M tokens is enough to do a lot, but the Lean graphs they are making are way too big to fit, so an LLM will never have the complete picture.