3 ms·

is there a simpler version of LEAN suitable for high school student level math? Sympy?

• deadbeef57 5y ago
  You might enjoy http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game... It's a game implemented in lean, where you work your way through the basic facts about natural numbers.
• Tainnor 5y ago
  sympy is not a proof assistant, but a symbolic computer algebra system
  • est 5y ago
    Well I'd say it's enough to automatically solve many high-school level problems, automatically. Like a poor man's Mathematica or WolframAlpha.
    • mkl 5y ago
      Yes, but that's a totally different category of problem from what proof assistants do.