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

Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

quantamagazine.org

Post reply on HN
Print view View original

251–260 of 275 posts

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#251

Post by yaantc »

abenedic wrote: post #190
abenedic wrote: post #189

Earlier quoted context omitted.

>not an inherent limitation of all backlit displays everywhere. This may be true, but in my experience(not very wealthy, typically sub $400 devices) the presets are set such that 0% backlight in the OS is glaringly bright. I cannot turn it down without rooting the device.

Maybe for tech device things we should have two separate tracks, one for wealthy snd people who can modify devices and one for poor and people who cannot. Even my Thnkpad laptop under Ubuntu has a setting for 10% brightness which is far too high for a truly dark room. The next lowest setting is 0% which is absolute dark. How do you use your laptop under such conditions?

You could use xbacklight to have a finer control of the display brightness. You can also rebind the brightness keys to shell scripts that use "xbacklight -inc " or -dec, with a finer resolution.

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#252

Post by Myrmornis »

arunix wrote: post #238
Myrmornis wrote: post #192

Earlier quoted context omitted.

I’ve been studying undergrad maths for the last year or two, and I had a bit of a breakthrough when I realized how much more effective it was for me to do all my work (notes, exercises) in LaTeX rather than with pen and paper. I can refactor at will, improving proofs, and the consistent tidy typesetting makes me think more systematically about the problem I’m working on.

What tool(s) do you use for working with LaTeX?

A Makefile to encapsulate all the details of how to generate the PDFs.

Text editor customizations to trigger `make .pdf` on save. (Emacs in my case)

A PDF viewer that reloads the PDF when it changes on disk (Skim in my case, which does auto-reload, but I also have some Applescript in the Makefile to poke Skim so that it notices the file change faster).

A good text editor LaTeX editing mode (Emacs in my case).

Random test editor customizations for working on LaTeX.

My main tips are

1. don't be shy of perfecting your work environment

2. use git to track both your work environment customizations and your LaTeX work.

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#253

Post by Jweb_Guru »

mannykannot wrote: post #242
Jweb_Guru wrote: post #231

Earlier quoted context omitted.

Oh, come on. "It's not any easier than writing a bug-free program" is not even remotely true. Getting the spec right is way easier than getting the implementation right, in almost all cases. And the logic isn't that different from set theory--there's even a set theoretic model (which you get when you use Prop, to which you can add classical axioms).

If getting the spec right is way easier than getting the implementation right, then strict waterfall would be the most effective way to write programs, and the holy grail of software engineering would be to automate the process of generating implementations from formal specs (there are some people who think exactly that, but that has been the case for about five decades, with effectively no impact on how software is…

I have no idea where you're going with this, but getting the spec right is very different from actually finding a proof for it. I never said actually finding the proof was always easy. But I will say this for sure: getting the spec right and finding a proof for it are jointly much easier than writing a nontrivial bug-free program without a theorem prover. The success or lack of success of waterfall is not relevant here, as that has very little to do with formal verification; additionally, the success of most software methodologies is not measured solely on whether the end product was correct.

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#254

Post by czei002 »

danharaj wrote: post #50
vbezhenar wrote: post #42

Earlier quoted context omitted.

I don't really understand why the entire known mathematics is not automatically proven yet. We, people, understand very formal proofs. Mathematics is very strict science with axioms and following theorems. It should be a perfect application for computing. I'm not talking about computer prooving theorem himself, but mathematician should write proof using some formal language and computer should be able to follow that…

> Mathematics is very strict science with axioms and following theorems. Mathematics textbooks would be intractably longer if they spelled out every step in explicit, formal detail. And then the proofs wouldn't make sense to people because the core ideas would be obscured by the formality! A typical mathematics proof is intended to be read by a thinking human assumed to have some level of mathematical sophistication…

Can't you make the formal proof software "smart" enough to prove a theorem given sufficient intermediate steps and hints about what other theorems/defs to use? i.e. basically what a book does? This would makes writing formal proof much easier, wouldn't it?

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#255

Post by busyant »

busyant wrote: post #187
fjsolwmv wrote: post #148

Earlier quoted context omitted.

It's sufficient for Mochizuki. Everyone else can decide for themselves what is sufficient for them.

> It's sufficient for Mochizuki. Everyone else can decide for themselves This sounds like a variant of the Turing test. Mochizuki and your pet dog both claim to have proven the ABC conjecture. The ABC conjecture has been proven when you can understand one proof but not the other.

I can't edit my post, but I should have phrased it more pithily:

Mochizuki and your pet dog both claim to have proven the ABC conjecture. The ABC conjecture has been proven when you can tell the difference between the two proofs.

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#256

Post by thanatropism »

rofo1 wrote: post #234
thanatropism wrote: post #91

Earlier quoted context omitted.

I once tried proving the very first theorem in Cannas da Silva's book of symplectic geometry in this style. Screw that. The proof that I eventually used in my dissertation is even wordier and with less display-mode equations than the one in the book (I became very influenced by the prose in old topology books). Most of the time, the point of proofs isn't to establish something is true, but to communicate something ab…

Which topology books contain prose, in your opinion?

General Topology by Munkres is a good example because it has a great deal of prerequisites covered in the first chapters so you can compare how he explains eg set theory, functions, equivalence classes with what something like Wikipedia gives.

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#257

Post by Retra »

alimw wrote: post #232
singularity2001 wrote: post #210

Earlier quoted context omitted.

Would it be possible to simplify the system by making default assumptions about a consensus/common-sense logic? Are topologists interested in different logical foundations?

You're right (and the GP isn't). A proof of your topological theorem in any one of Coq/Isabelle/Lean is a pretty good indication that it's correct, in spite of their various foundations.

... assuming you correctly wrote your theorem in those frameworks.

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#258

Post by Retra »

Jweb_Guru wrote: post #231
Retra wrote: post #169

Earlier quoted context omitted.

The painful part is that you're using tools which are trying to bridge between wildly different logical foundations. Just because a computer beeps and says "proof correct" doesn't mean you've proven what you thought you have, so we need to first translate the logic in which your assumptions are derived into the logic of the machine. That is a complex and subtle project. In other words, it's actually very easy to prov…

Oh, come on. "It's not any easier than writing a bug-free program" is not even remotely true. Getting the spec right is way easier than getting the implementation right, in almost all cases. And the logic isn't that different from set theory--there's even a set theoretic model (which you get when you use Prop, to which you can add classical axioms).

If programmers sat around writing <10K line pure programs with no user interaction, they would have just as lovely a time as Mathematicians. If theorem proving in mathematics is easy for you, it is because your aren't trying to prove hard things.

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#259

Post by Retra »

zakk wrote: post #239
proto-n wrote: post #237

Earlier quoted context omitted.

Except that he doesn't say it is incorrect, he says that "it seems bizarre" to him that seemingly Michozuki's paper doesn't have any uses beyond proving the ABC conjuncture. The rest of this comment is just explaining how it's usually not like this.

When the world's most brilliant mathematician (or at least one of the most brilliant) says "it would be rather bizzarre if your argument worked" the implications are absolutely clear. As a scientist I would never make such a statement, moreso for a theory I admittedly don't understand. Tangentially, it's not Tao's case, but I have seen a lot of bullying in the academia along these lines... "I am not saying it's wrong…

Is it not bizarre?

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#260

Post by Jweb_Guru »

Retra wrote: post #258
Jweb_Guru wrote: post #231

Earlier quoted context omitted.

Oh, come on. "It's not any easier than writing a bug-free program" is not even remotely true. Getting the spec right is way easier than getting the implementation right, in almost all cases. And the logic isn't that different from set theory--there's even a set theoretic model (which you get when you use Prop, to which you can add classical axioms).

If programmers sat around writing <10K line pure programs with no user interaction, they would have just as lovely a time as Mathematicians. If theorem proving in mathematics is easy for you, it is because your aren't trying to prove hard things.

Getting a spec right is not the same as proving a theorem. It is the same as stating a theorem. And I absolutely disagree with you that making small pure programs magically makes them bugfree.
Post reply on HN