/sci/ - Science & Math » Thread #13222509

66KiB, 504x845, phpDXecwm.png

View Same Google iqdb SauceNAO

So I've noticed that nobody wants to type formal proofs into a computer...

Anonymous Tue 01 Jun 20:08:19 2021 No.13222509 View Reply Original Report

Quoted By: >>13222536 >>13222563 >>13224114

...what does this say about dramatic predictions about the future of computer math that were common a little over a decade ago??

You can't get computers to process data if mathematicians are too lazy to type them in...

Anonymous

Anonymous Tue 01 Jun 2021 20:13:42 No.13222527 Report

Quoted By: >>13222536

computers are a fad writing thigns down on paper is faster and less hassle
when our interface with computers is writing things on paper then it will pick up, but we need paper thin touch sensitive screens for that to become a reality since the ease of paper is the physical manipulation of it. tabs or other screen-based schemes are not as rapid

Anonymous

Anonymous Tue 01 Jun 2021 20:16:25 No.13222536 Report

Quoted By: >>13222579

>>13222527
>writing thigns down on paper
for quick trying things out maybe. Even for taking notes that should last over 2 weeks, I go to some latex.

>>13222509
It's indeed not widespread (because it's not fun) but I don't see it as a blocker for it developing

Anonymous

Anonymous Tue 01 Jun 2021 20:23:30 No.13222563 Report

Quoted By: >>13224274

>>13222509
maths are low-iq and haven't even taken the plover plunge, something even a woman knows. Your keyboard is the beating heart of your computer, but it was designed for secretaries many decades ago.

Anonymous

Anonymous Tue 01 Jun 2021 20:27:25 No.13222579 Report

Quoted By:

>>13222536
here's the issue: you type a computer program into a computer, it's great because you get to play with it
you type a (for example: Fitch style) derivation into a computer, it sucks because all you can do is check if you made a mistake...and nobody has a use for correct derivations anyway
so when it comes to doing anything formal, the computer program wins every time because the only thing you can do with the derivation is feed it into a glorified spell checker and see if you made any mistakes
I mean, if you can't go to school normally, you could in theory learn a subject area of math by typing the solution to every homework problem into a derivation checker on your computer...but nobody even suggests that, it's pure fiction...

Anonymous

Anonymous Wed 02 Jun 2021 04:20:38 No.13224114 Report

Quoted By:

>>13222509
They use proof assistants (Agda for example) all the time and there's a team right now at CMU writing a cubical type theory proof assistant for real numbers. This will forever be a thing because of Voedvodsky

Anonymous

Anonymous Wed 02 Jun 2021 05:21:31 No.13224274 Report

Quoted By:

>>13222563
Plover? like the bird? What are you on about?

Capcode	All Only User Posts Only Moderator Posts Only Admin Posts Only Developer Posts
Show Posts	All Only With Images Only Without Images
Deleted Posts	All Only Deleted Posts Only Non-Deleted Posts
Ghost Posts	All Only Ghost Posts Only Non-Ghost Posts
Post Type	All Only Sticky Threads Only Opening Posts Only Reply Posts
Results	All Grouped By Threads
Order	Latest Posts First Oldest Posts First

Your latest searches