A Rust implementation of the Lean kernel
Yatima grinned triumphantly, and recounted vis chain of reasoning. Radiya said calmly:
"Good. You've just discovered the Gauss-Bonnet Theorem, linking the Euler number and total curvature."
"Really?" Yatima felt a surge of pride; Euler and Gauss were legendary miners - long-dead fleshers, but their skills had rarely been equaled.
"Not quite." Radiya smiled slightly. "You should look up the precise statement of it, though; I think you're ready for a formal treatment of Riemannian spaces. But if it all starts to seem too abstract, don't be afraid to back off and play around with some more examples."