Unicode in Zulip

Stream: general

[Johan Commelin]

Quick question: how do I comfortably input unicode in Zulip? So far I have used copy-paste to write alphas and betas. In VS code these are magically replaced with unicode... in the rest of my life TeX does this for me. How do I get them here?

[Mario Carneiro]

You can use tex here, although it gets math font: $\alpha$

[Johan Commelin]

Ok, thanks.

[Johan Commelin]

Test: $\alpha$ $\alpha$

[Johan Commelin]

Hmm, neither do what I want...

[Johan Commelin]

How do you input an alpha in code? So between back-ticks?

[Johan Commelin]

Test: $\alpha$

[Patrick Massot]

I use https://github.com/docwhat/itsalltext/tree/release-1.9.3#readme It gives me a small "edit" button near textareas in firefox. Clicking this button fires vim and you can type whatever you want

[Patrick Massot]

Of course you can also configure it to fire emacs if that's your religion

[Johan Commelin]

No, I'm a vimmer. But I never input alphas directly into vim...

[Johan Commelin]

I was an ascii-only guy, until I met Lean

[Johan Commelin]

At some point, someone will formalise Fermat's last theorem in Lean

[Patrick Massot]

Then you should go and configure your vim to make you a unicode guy

[Johan Commelin]

And it will take us 5 years to figure out that they spoofed us with an punycode attack: https://en.wikipedia.org/wiki/IDN_homograph_attack

[Johan Commelin]

Importing some library whose name looks completely familiar, but inside the library they do just assume false...

[Patrick Massot]

I think Kevin decided we weren't formalizing FLT in the end

[Patrick Massot]

This is too old

[Patrick Massot]

He works on perfectoid spaces

[Johan Commelin]

The problem remains... whether you are formalising the latest hotness in the Langlands program, or some hardcore $\infty$-stuff, or something from quantisation-blabla... unicode is ambiguous and susceptible to social attacks...

[Johan Commelin]

Anyway, I will stuff away my tinfoil hat... enough other problems to focus on right now (^;

[Kevin Buzzard]

I don't think it's too difficult to formalise. The proof might be harder though.

[Kevin Buzzard]

The thing about the proof is that there is a huge amount of analysis that goes into the trace formula

[Kevin Buzzard]

and I know of no proof which ultimately avoids the trace formula

[Kevin Buzzard]

in the non-compact case I should add -- SL(2).

[Patrick Massot]

https://github.com/formalabstracts/formalabstracts/blob/master/fabstract/Wiles_A_and_Taylor_R_FermatLast/fabstract.lean

[Kevin Buzzard]

It's the one part of the proof I've not read and it would not surprise me if I went to my grave not having read it.

[Kevin Buzzard]

Unless EPSRC give me several million quid to formalise it.

[Patrick Massot]

Statement is already done :smile:

[Kevin Buzzard]

Oh OK that's great, we're half way there.

[Patrick Massot]

Indeed

[Johan Commelin]

Lol, they have a type called document

[Johan Commelin]

That's fantastic (^;