ZLB

My favorite experimental cinema/visual music director, Ken Jacobs, is being shown in tank.tv an online gallery during october. Profit from this rare opportunity ! I had the opportunity to view his work live in the February’s Amsterdam Sonic Acts XII and he blew my mind away !

ps: thanks to pablo for the tip.

edit: I’ve posed a question to Ken: Q:

Some of your work, namely using the nervous magic lantern system, is happening for the first time as it is made, as light projected on a screen, something which is inherently difficult to capture and document. Nevertheless it’s very important that this work is documented and available in the future: how do you resolve this dilemma ?

see the answer here.

VDash is a project to create a formalized math commons. It will be wiki style website with internal proof verification. It seems very exciting, specially the possibility that one day a AI robot mathematician will have access to all mathematic proofs made and work from there towards new results. 

1. theorem "( a :: int ) dvd b ==> a ^ n dvd b ^ n" proof - assume "a dvd b" show "a ^ n dvd b ^ n" proof ( induct n ) show "a^0 dvd b^0" proof - have "a^0 = 1" by ( rule power_0 ) moreover have "( 1 dvd b ^ 0 )" by ( rule zdvd_1_left) ultimately show ?thesis by simp qed next fix n assume "a ^ n dvd b ^ n" show "a ^ Suc n dvd b ^ Suc n" proof - from prems have "a * a ^ n dvd b * b ^ n" by ( intro zdvd_zmult_mono ) moreover have "a ^ Suc n = a * a^n" by ( rule power_Suc ) moreover have "b ^ Suc n = b * b^n" by (rule power_Suc) ultimately show ?thesis by simp qed qed qed

check also Isar - Intelligible semi-automated reasoning