This chapter discusses the controversial viewpoints surrounding the Lean theorem prover's foundational aspects, highlighting skepticism from some community members regarding its consistency. The speakers express confidence that these concerns are largely insignificant to the broader mathematical community, which prioritizes practical applications over foundational debates.