Tutorial for Isabelle/HOL https://isabelle.in.tum.de/doc/tutorial.pdf states that:
HOL can express most mathematical concepts, and functional programmingis just one particularly simple and ubiquitous instance.
What is the example of concept that can not be expressed (reasoned) in Isabelle/HOL? What is the example of logic that can not be embedded (expressed) in Isabelle/HOL?
I am trying to use Isabelle/HOL for implementing artificial general intelligence and I would like to comprehend the possible bounds of the framework.