My layman understanding of Godel's Incompleteness Theorem is that you are correct. It states that there are things that are true but no proof can exist (providable by human or AI provers).