> LLMs did scale with huge data, symbolic AI did not.
Symbolic AI have not had a privilege to be applied or "trained" with huge data. 30 millions assertions is not a big number.
This is correct. Those 30M assertions were basically entered by hand.