News for hackers. Stuff that matters.

A comment on Mathematicians welcome computer-assisted proof in ‘grand unification’ theory.

Re:Mathematicians welcome computer-assisted proof in ‘grand ... by est on Saturday June 19, 2021 @01:47PM (#27562595)
is there a simpler version of LEAN suitable for high school student level math? Sympy?
[ Parent | on HN ]
Re:Mathematicians welcome computer-assisted proof in ‘grand ... by deadbeef57 on Saturday June 19, 2021 @01:52PM (#27562641)
You might enjoy 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.

[ Parent | on HN ]
Re:Mathematicians welcome computer-assisted proof in ‘grand ... by Tainnor on Saturday June 19, 2021 @01:55PM (#27562689)
sympy is not a proof assistant, but a symbolic computer algebra system
[ Parent | on HN ]
Re:Mathematicians welcome computer-assisted proof in ‘grand ... by est on Sunday June 20, 2021 @12:44AM (#27567135)
Well I'd say it's enough to automatically solve many high-school level problems, automatically. Like a poor man's Mathematica or WolframAlpha.
[ Parent | on HN ]
Re:Mathematicians welcome computer-assisted proof in ‘grand ... by mkl on Sunday June 20, 2021 @08:28AM (#27569352)
Yes, but that's a totally different category of problem from what proof assistants do.
[ Parent | on HN ]