Zulip Chat Archive

Stream: general

Topic: Lean's proof of FTA is "obviously wrong"


view this post on Zulip Kevin Buzzard (May 10 2020 at 13:28):

This has come up before, but this time it's pretty horrible, at least I think it is.

Take a look at the docs for complex.exists_root, the Lean proof of the fundamental theorem of algebra. Read the statement of the theorem. You see what it says about all polynomials having a root? What about the polynomial f(z)=37f(z)=37? It has degree 0 and no root.

Exercise: what is going on?

view this post on Zulip Shing Tak Lam (May 10 2020 at 13:30):

The theorem requires 0 < degree f? So f(z) = 37 has degree 0 and isn't accepted?

view this post on Zulip Reid Barton (May 10 2020 at 13:31):

Good point. The theorem ought to say 1 ≦ f.degree.

view this post on Zulip Shing Tak Lam (May 10 2020 at 13:32):

image.png

This is a less than sign which is underlined, not a less than or equal sign...

view this post on Zulip Chris Hughes (May 10 2020 at 13:33):

I think it would be good to get rid of that underlining.

view this post on Zulip Reid Barton (May 10 2020 at 13:33):

Interesting, it looks less bad here:
image.png

view this post on Zulip Shing Tak Lam (May 10 2020 at 13:37):

I just tried a few different browsers, Firefox (posted above) has a thick underline, (old) Edge and Internet explorer has a thin underline. So this isn't consistent across browsers...

view this post on Zulip Kevin Buzzard (May 10 2020 at 13:37):

Yes. The underlying issue apparently turning \lt into \le has been discussed before here, but it still made me look twice. IIRC the conclusion was that people didn't really know what to do instead, and some people weren't bothered by it.

view this post on Zulip Chris Hughes (May 10 2020 at 13:38):

use a different colour for the links?

view this post on Zulip Chris Hughes (May 10 2020 at 13:38):

Or just not highlight them at all?

view this post on Zulip Shing Tak Lam (May 10 2020 at 13:38):

(duplicate)

view this post on Zulip Kevin Buzzard (May 10 2020 at 13:39):

Ideally one would use a colour which, when clicked, does not turn into a dark purple which looks like a black. But light blue generally works for stuff like this, doesn't it? As long as it stayed light blue?

view this post on Zulip Reid Barton (May 10 2020 at 13:43):

The link color and visited link color can be set independently.

view this post on Zulip Patrick Massot (May 10 2020 at 13:43):

My answer is always the same: remove all link decoration here. Every word is a link, what's the point?

view this post on Zulip Shing Tak Lam (May 10 2020 at 13:55):

image.png
image.png
image.png

Here's a few images of what it'd look like without the underlines

  1. black links
  2. darkblue links
  3. lightblue links (obviously not using this)

Also with the setup right now, the links in the centre section should stay the same colour even after it has been clicked. The ones to the sides will change to purple, but that's separate.

view this post on Zulip Kevin Buzzard (May 10 2020 at 13:56):

Are there any <s in your examples?

view this post on Zulip Patrick Massot (May 10 2020 at 13:57):

Maybe darkblue is a good compromise

view this post on Zulip Patrick Massot (May 10 2020 at 13:57):

And all of them are better than underlines, including the awful light blue version

view this post on Zulip Shing Tak Lam (May 10 2020 at 13:58):

image.png

This one has <

view this post on Zulip Rob Lewis (May 10 2020 at 14:18):

Yes, this has come up before. It never looked very confusing on my browsers so I didn't really think about it. My preferred solution would be to remove underlining, keep the same colors as now, and make sure that the link colors change (subtly, not to blue or anything) on mouseover. I think they already do this.

view this post on Zulip Rob Lewis (May 10 2020 at 14:19):

I'm happy to accept a PR to the CSS changing this. Actually, I had a vague memory of there being a PR already, but I don't see it.

view this post on Zulip Ryan Lahfa (May 10 2020 at 14:20):

Rob Lewis said:

I'm happy to accept a PR to the CSS changing this. Actually, I had a vague memory of there being a PR already, but I don't see it.

Well, I wanted to do one in some topic, so I have a custom CSS userscript to remove those underlines personally and show them only on hover. It works pretty fine, I can bundle it into a PR.

view this post on Zulip Ryan Lahfa (May 10 2020 at 14:21):

Basically I just apply

.decl_type a:link, .structure_field a:link {
    text-decoration: none !important;
}

.decl_type a:hover, .structure_field a:hover {
    text-decoration: underline !important;
}

on mathlib (I can remove the !important in the PR of course.)

view this post on Zulip Rob Lewis (May 10 2020 at 14:22):

Sounds good to me.

view this post on Zulip Shing Tak Lam (May 10 2020 at 14:26):

I think this is where the new line should go? At least that's how I made those examples above

view this post on Zulip Ryan Lahfa (May 10 2020 at 14:27):

Shing Tak Lam said:

I think this is where the new line should go? At least that's how I made those examples above

I could put it there, @Rob Lewis what do you think?

view this post on Zulip Ryan Lahfa (May 10 2020 at 14:27):

@Shing Tak Lam Well if you've done the work, I can let you send the PR if you want :)

view this post on Zulip Shing Tak Lam (May 10 2020 at 14:28):

I haven't. I just used Firefox dev tools, which changes the page as I edit the CSS.

view this post on Zulip Ryan Lahfa (May 10 2020 at 14:28):

Shing Tak Lam said:

I haven't. I just used Firefox dev tools, which changes the page as I edit the CSS.

Oh okay

view this post on Zulip Rob Lewis (May 10 2020 at 14:29):

Yep! That looks right. It should be a very easy PR, you can even do it with the Github web editor.

view this post on Zulip Ryan Lahfa (May 10 2020 at 14:30):

I want to test before to send it, just to ensure I don't break anything, so I've forked and will send the PR soon :)

view this post on Zulip Shing Tak Lam (May 10 2020 at 14:30):

(and if you want to have an underline when hovering, I think it's Line 233 just below where I linked)

view this post on Zulip Rob Lewis (May 10 2020 at 14:31):

Thanks!

view this post on Zulip Ryan Lahfa (May 15 2020 at 21:35):

@Rob Lewis https://github.com/leanprover-community/doc-gen/pull/20 :)


Last updated: May 14 2021 at 22:15 UTC