learning from a chatbot is definitely possible (i am using it for learning) but it requires approaching it with an adversarial mindset and only works in fields where you can verify the result
RE:
fun fact: Lean can represent real numbers
not floats (although Lean can do them). not doubles. not even arbitrary precision floats, but *actual* reals — which includes the squared root of 2, the exact number Pi (not an approximation!), fractions like 0.111... and so on.
this still blows my mind
)
