Fortnightly links (93)

Martin Kalck, Nebojsa Pavic, Evgeny Shinder: Obstructions to semiorthogonal decompositions for singular threefolds I: K-theory is a really interesting paper, giving obstructions (and exhibiting many examples in natural examples!) to having a Kawamata-style semiorthogonal decomposition for singular varieties. This generalises the case for surfaces, via an interesting relationship between negative K-theory and the Brauer group. Cool stuff.

Qingyuan Jiang: On the Chow theory of projectivization discusses isomorphisms at the level of integral Chow groups arising from semiorthogonal decompositions. The cool thing is that this is usually not what is to be expected from semiorthogonal decompositions, so this is exciting.

Kevin Buzzard: Can computers prove theorems? explains how formal proof verification can be considered a game, and actually provides a game-environment for defining the natural numbers!

Do you think we can get the speed running community interested in formalising the proof of Fermat's last theorem? After all, the level has a perfectly good definition, which reads

theorem FLT (a b c n : ℕ) (h : n > 2) : a ^ n + b ^ n = c ^ n → a * b = 0 :=
begin
  -- insert millions of lines of code here
end