Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Software for Math Research

amathr.org

Post reply on HN
Print view View original

21–30 of 31 posts

Re: Software for Math Research

#21

Post by sadfev »

outlace wrote: post #6

No proof assistants like Lean and Coq?

I was wondering about that too. They are perhaps most important tools for both CS and pure mathematics.

It’s very interesting that Lean has exploded in the mathematics community. Kevin Buzzard talks about it a lot, but I haven’t seen a talk which explains why Lean succeeded in creating a gargantuan math library whereas Coq only recently got respectable math library in “MathComp” (I am also including Analysis library).

I would like to know apart from social reasons what technical choices lead to Lean dominating (ordinary/regular/pure) mathematics.

I hear “quotients” but no one actual explains with a concrete example.

Re: Software for Math Research

#22

Post by prirai »

ai_ia wrote: post #15

The list is missing Manim for visualization. I tried it out because I was curious how 3b1b creates his videos and was blown away by the simplicity of the tool. For simple visualization and teaching aid, Manim is a great tool.

Adidng this to my list. Thanks. Btw I use Sage and it has most of the packages written below.

Re: Software for Math Research

#23

Post by prirai »

MayeulC wrote: post #14

xcas is very good (though the UI shows its age), based on giac: https://www-fourier.univ-grenoble-alpes.fr/~parisse/giac.htm... In addition to software in the comments, not even WolframAlpha is listed.

The list mentions free software alternatives, not the proprietary ones which would be probably on everyoneeveryone's mouths.

Re: Software for Math Research

#24

Post by billfruit »

linspace wrote: post #13
agambrahma wrote: post #10

Recently (re-)discovered Mathematica, and found spanning a much larger set of domains than I expected (also, very approachable).

The first time I used Mathematica (20 years ago) it blew my mind. To be fair it was the first time I used a CAS and so the very idea of a computer crushing me at several calculus tasks was incredible. From the open source alternatives the better supported I think is (wx)Maxima, which for the simple tasks I usually require (i.e some Taylor series, check cumbersome trigometric equations, ...) it's more than enough alth…

What about Axiom, it seems to have been worked on for many decades.

Re: Software for Math Research

#26

Post by maxwells-daemon »

sadfev wrote: post #21
outlace wrote: post #6

No proof assistants like Lean and Coq?

I was wondering about that too. They are perhaps most important tools for both CS and pure mathematics. It’s very interesting that Lean has exploded in the mathematics community. Kevin Buzzard talks about it a lot, but I haven’t seen a talk which explains why Lean succeeded in creating a gargantuan math library whereas Coq only recently got respectable math library in “MathComp” (I am also including Analysis library)…

In my experience: one of Lean's main advantages is developer experience. It's convenient by design, with lots of automation to make easy proofs trivial. You do your work in VSCode or Emacs rather than some outdated IDE, and the server mode makes it easy(ish) to integrate with other software.

Re: Software for Math Research

#27

Post by outlace »

sadfev wrote: post #21
outlace wrote: post #6

No proof assistants like Lean and Coq?

I was wondering about that too. They are perhaps most important tools for both CS and pure mathematics. It’s very interesting that Lean has exploded in the mathematics community. Kevin Buzzard talks about it a lot, but I haven’t seen a talk which explains why Lean succeeded in creating a gargantuan math library whereas Coq only recently got respectable math library in “MathComp” (I am also including Analysis library)…

I think it all comes down to the aesthetics and user experience. The Lean webpage is inviting and modern. Coq’s website looks like it’s from the 90s. Lean’s integration with Visual Studio Code is clean and user friendly. The language itself is familiar and polished. The imprimatur of a Microsoft team producing Lean being makes it seem more sophisticated.

Re: Software for Math Research

#28

Post by coolgeek »

amathres_info wrote: post #19

I think you are all missing the context here. The "Association for Mathematical Research" is a new organization created by various people who got in trouble on woke math twitter. Nobody had heard of it until yesterday. (Their crimes are mostly opposing diversity statements in job applications, or favoring gifted programs.) It looks like a schism with the AMS (which more-or-less publicly takes the opposite view on the…

> Their crimes are ... favoring gifted programs

I looked around on the AMS site, and I'm not seeing anything about the AMS opposing gifted education. Would you please provide a link to this?

(To be perfectly clear, I do not want links to opposition in the wider world. I've come across references to that before. I just find it hard to believe that the AMS would oppose gifted education.)

Re: Software for Math Research

#29

Post by sadfev »

maxwells-daemon wrote: post #26
sadfev wrote: post #21

Earlier quoted context omitted.

I was wondering about that too. They are perhaps most important tools for both CS and pure mathematics. It’s very interesting that Lean has exploded in the mathematics community. Kevin Buzzard talks about it a lot, but I haven’t seen a talk which explains why Lean succeeded in creating a gargantuan math library whereas Coq only recently got respectable math library in “MathComp” (I am also including Analysis library)…

In my experience: one of Lean's main advantages is developer experience. It's convenient by design, with lots of automation to make easy proofs trivial. You do your work in VSCode or Emacs rather than some outdated IDE, and the server mode makes it easy(ish) to integrate with other software.

I think CoqIDE is great and ProofGeneral (Emacs) is something all Coq experts use.

I have the opposite experience with Lean 4, the VSCode integration is horrid and documentation is awful.

The only good sources are papers for Lean4.

Granted I can go back to Lean3 but why would I?

Re: Software for Math Research

#30

Post by outlace »

sadfev wrote: post #29
maxwells-daemon wrote: post #26

Earlier quoted context omitted.

In my experience: one of Lean's main advantages is developer experience. It's convenient by design, with lots of automation to make easy proofs trivial. You do your work in VSCode or Emacs rather than some outdated IDE, and the server mode makes it easy(ish) to integrate with other software.

I think CoqIDE is great and ProofGeneral (Emacs) is something all Coq experts use. I have the opposite experience with Lean 4, the VSCode integration is horrid and documentation is awful. The only good sources are papers for Lean4. Granted I can go back to Lean3 but why would I?

But Lean4 is in alpha stage and there are no official stable releases yet, of course it's not well-documented nor polished yet. Lean3 works perfectly well and has everything you need.
Post reply on HN