MO editors' lounge

« first day (1856 days earlier) ← previous day next day → last day (2066 days later) »

6:23 AM

I'd guess that since the original post on MO has been edited to gibberish and there now already is a post by the same user, the MO post can be safely deleted. (Perhaps rollback could be reasonable too, but I do not really see the point in keeping that post around.)

-5

Q: kopokjjjjjjjjjjjjjjjjjjjj

oko;joooooooooooooooookkkkkkkkkkkkkkkkkk

-1

Q: Deciphering coded message knowing little about the encoding matrix

Hello, there was a matrix/cryptography problem I was unable to work out completely: 'Your task is to crack the following code and find the encrypted word. To make your task easier, the following information about the encoding matrix is given: Position 1,1 in the encoding matrix is an even num...

matrices matrix-equations matrix-calculus cryptography

5 hours later…

Martin Sleziak

10:57 AM

specific-question A new tag lean-theorem-prover was created here: Which mathematical definitions should be formalised in Lean? I guess the more general tag proof-assistants would be a reasonable fit too.

Q: Which mathematical definitions should be formalised in Lean?

The question. Which mathematical objects would you like to see formally defined in version 3.4.1 of the Lean Theorem Prover? Examples. Topological groups have been done, schemes have been done, Noetherian rings got done last month, Noetherian schemes have not yet been done (but are probably n...