Lean's proof of FTA is "obviously wrong"

Stream: general

[Kevin Buzzard]

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)=37$? It has degree 0 and no root.

Exercise: what is going on?

[Shing Tak Lam]

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

[Reid Barton]

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

[Shing Tak Lam]

image.png

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

[Chris Hughes]

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

[Reid Barton]

Interesting, it looks less bad here:
image.png

[Shing Tak Lam]

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...

[Kevin Buzzard]

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.

[Chris Hughes]

use a different colour for the links?

[Chris Hughes]

Or just not highlight them at all?

[Shing Tak Lam]

(duplicate)

[Kevin Buzzard]

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?

[Reid Barton]

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

[Patrick Massot]

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

[Shing Tak Lam]

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.

[Kevin Buzzard]

Are there any <s in your examples?

[Patrick Massot]

Maybe darkblue is a good compromise

[Patrick Massot]

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

[Shing Tak Lam]

image.png

This one has <

[Rob Lewis]

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.

[Rob Lewis]

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.

[Ryan Lahfa]

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.

[Ryan Lahfa]

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.)

[Rob Lewis]

Sounds good to me.

[Shing Tak Lam]

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

[Ryan Lahfa]

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?

[Ryan Lahfa]

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

[Shing Tak Lam]

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

[Ryan Lahfa]

Shing Tak Lam said:

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

Oh okay

[Rob Lewis]

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

[Ryan Lahfa]

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 :)

[Shing Tak Lam]

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

[Rob Lewis]

Thanks!

[Ryan Lahfa]

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