/sci/ - Science & Math » Thread #13461375

703KiB, 873x1079, 1525955202473.png

View Same Google iqdb SauceNAO

Formal Math System

Anonymous Mon 02 Aug 06:52:58 2021 No.13461375 View Reply Original Report

Quoted By: >>13462135 >>13463093 >>13463152 >>13466524

Are there any good formal systems for doing maths?

I'm a programmer and the fact that maths do not have a unified formalized system with syntax and grammar macros bothers me.

Anonymous

View Same Google iqdb SauceNAO seed0040.png, 352KiB, 512x512

Anonymous Mon 02 Aug 2021 07:07:03 No.13461412 Report

Quoted By: >>13461428

https://leanprover.github.io/introduction_to_lean/

It actually makes math really fun when it's just writing computer programs.

Anonymous

View Same Google iqdb SauceNAO Screenshot 2021-08-02 at 00-09-1 (...).png, 128KiB, 780x2441

Anonymous Mon 02 Aug 2021 07:11:47 No.13461428 Report

Quoted By:

>>13461412
It strikes me that reading pic related is going to be a better introduction to writing proofs for students coming from computer science than a book like Velleman's how to prove it, because computer science are already comfortable with using deductive logic in their programs, but the flowerly writing of mathematicians can throw them for a loop and convince them that they are missing some piece of the puzzle. A proof is really just a program written in the language of colloquial deductive logic.

Anonymous

Anonymous Mon 02 Aug 2021 12:51:59 No.13462128 Report

Quoted By:

coq, agda, lean are all good formal systems based on type theory. coq has an older pedigree whereas lean is less purely type theory and more mathematician focussed. agda doesn't use tactics so it's more similar to writing a program than a proof. there's also loads of other formal systems but they don't use type theory so i don't care

Anonymous

Anonymous Mon 02 Aug 2021 12:56:02 No.13462135 Report

Quoted By: >>13462143

>>13461375
>what is mathematica

Anonymous

Anonymous Mon 02 Aug 2021 12:58:04 No.13462143 Report

Quoted By: >>13466445

>>13462135
mathematica is not a formal proof system

Anonymous

Anonymous Mon 02 Aug 2021 17:26:16 No.13463093 Report

Quoted By: >>13463119

>>13461375
>Are there any good formal systems for doing maths?
They tried to answer this about a century ago and it resulted in the incompleteness theorems

Anonymous

Anonymous Mon 02 Aug 2021 17:34:59 No.13463119 Report

Quoted By: >>13463184 >>13463199

>>13463093
cringe

Anonymous

Anonymous Mon 02 Aug 2021 17:46:00 No.13463152 Report

Quoted By:

>>13461375
Like cs does?

Anonymous

Anonymous Mon 02 Aug 2021 17:58:26 No.13463184 Report

Quoted By:

>>13463119
do you know what a formal system is

Anonymous

Anonymous Mon 02 Aug 2021 18:01:36 No.13463199 Report

Quoted By: >>13463211

>>13463119
why?

Anonymous

Anonymous Mon 02 Aug 2021 18:03:26 No.13463211 Report

Quoted By: >>13463311 >>13463313

>>13463199
Because people reflexively bringing up Gödel's incompleteness theorems as a reason to not care about formal systems is cringe.

Anonymous

Anonymous Mon 02 Aug 2021 18:28:44 No.13463311 Report

Quoted By: >>13463402

>>13463211
I don't think he said you shouldnt care
I think he's saying theres no "good" formal system
I also think he didnt read the OP properly, since OP is asing for programming-specific formal systems

Anonymous

Anonymous Mon 02 Aug 2021 18:29:20 No.13463313 Report

Quoted By: >>13463402

>>13463211
where did he say that one shouldn't care about formal systems?

Anonymous

Anonymous Mon 02 Aug 2021 18:54:23 No.13463402 Report

Quoted By: >>13463425 >>13463431 >>13464983

>>13463311
There are good ones.

>>13463313
Why would you bring up Gödel's incompleteness theorems glibly like that otherwise? There's a certain kind of person who always does that when formal systems get mentioned. They don't tend to know a lot about formal systems.

Anonymous

Anonymous Mon 02 Aug 2021 18:58:46 No.13463425 Report

Quoted By:

>>13463402
>There are good ones.
It depends how you define "good".
If you mean a unified formal system with syntax and grammar macros, I think lean fits that
If you mean a complete and consistent system that can answer and question, then there is no good system

Anonymous

Anonymous Mon 02 Aug 2021 18:59:47 No.13463431 Report

Quoted By:

Anonymous

Anonymous Tue 03 Aug 2021 03:04:50 No.13464983 Report

Quoted By: >>13465003

>>13463402
>mentioning incompleteness implies choice of formal system doesn't matter
sophmore that learned to counter-signal incompleteness cause 4chan told him it was "reddit"

Anonymous

Anonymous Tue 03 Aug 2021 03:11:30 No.13465003 Report

Quoted By:

>>13464983
It is comparable to bringing up the Hegelian Dialectic, in any context. Bunch of virtue signaling twat smokers.

Anonymous

Anonymous Tue 03 Aug 2021 06:14:04 No.13465387 Report

Quoted By: >>13465397

Ok here. Here are the qualities I want in the system:

>consistency not completeness
>formal proofing isn't important to me
>I am looking for a formal system I can write out by hand and solve like algebra
>ideally the syntax should be very similar to algebra
>it matters to !e that I can build differentiable structures like I can in algebra
>ideally I can take problems from my textbooks and solve these problems by had in this system
>I don't want it to.be too much more verbose than regular maths obviously because I am doing things by hand

Basically it.bothers me that there isn't an exact way to interpret problems in my textbook.

Anonymous

Anonymous Tue 03 Aug 2021 06:18:29 No.13465397 Report

Quoted By: >>13465908

>>13465387
Sounds like you want a computer algebra system. Axiom and Maxima are two free (libre) systems you might want to look into.

Anonymous

Anonymous Tue 03 Aug 2021 11:14:57 No.13465908 Report

Quoted By: >>13465915

>>13465397
How could you not mention Sage?

Anonymous

Anonymous Tue 03 Aug 2021 11:18:37 No.13465915 Report

Quoted By:

>>13465908
Never tried it, seemed bloated and convoluted to me. It's more like a meta-system, collating many others (like Maxima for example).

Anonymous

Anonymous Tue 03 Aug 2021 15:08:25 No.13466445 Report

Quoted By:

>>13462143
>programming languages have no formal proofs
>references compiler

Anonymous

Anonymous Tue 03 Aug 2021 15:33:47 No.13466524 Report

Quoted By:

>>13461375
Sounds like you're looking for something called a "proof assistant". Try Coq or Agda, you'll like them.

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