A very interesting issue of the American Mathematical Society on formal proofs.  

Most people don’t realize it but mathematical proofs are usually written in a very condensed way, that allows other mathematicians to understand what is being said, but which are not formal complete statements, since lots of things are implied. Proof verification is essentially  a social process by which other mathematicians convince themselves that the proof is correct. This doesn’t sound very reassuring but it has (in most cases) worked until now. Off course new challenges are appearing,  with proofs 500 pages long or that use computer programs to to part of the job (like testing cases), that’s why formal proofs are becoming more and more pertinent.

AMP – A very underrated shoegazing psychedelic (in the profound sense) rock ban. Maybe their lack of acknowledgment is due to their name making it quite hard to find them in web searches.  Astralmoonbeamprojections is a very special album with drony soundscapes and timeless streams of guitar. The more rhythmic but nevertheless freaky Saint Cecilia Sinsemilla will also propel you to higher layers of the stratosphere.

Aube Reworks – This series of releases by Aube (aka, Akifumi Nakajima) are just a pleasure to listen to. All of them rework albums from other artists such as Maurizio Bianchi. The albums focus a lot on heavy repetition of little fragments of sound which slowly unfold to dense layers of sound.

Very interesting book containing articles originally published in the Village Voice by composer Tom Johnson. It can be downloaded here. Another interesting book by the author on mathematics and composition is Self-similar melodies.

I was delighted to finally find a video of this device in action. I’ve been fascinated by it for some time, because it was really one of the first “rhythm machines” ever made. It’s very interesting to think that such radical sound machines were already being made and played in 30′s.  The Rhythmicon was commissioned by composer Henry Cowell and built by Theramin. Now if I could get my hands on a performance of the “Rhythmicana (Concerto for Rhythmicon and Orchestra; 1931)”, that would would be nice.

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

the fourth dimension

I’m fascinated with this effect. A lot of examples of slit scanning here.

Yes, this last weekend’s Todaysart Festival 2008 has reminded me that it’s been one year since i first started learning supercollider. What are my thoughts, after one year of usage ? 

1. I never want to go back to patching in max !
2. (unless i need to do something fast, off course)
3. Supercollider allows meone to make complex structures, with dynamic scalability very easily. Being free from the constraints of patching means that dealing with something that has one input, 100 inputs, or whose inputs are not even know at this moment is easy. In terms of arrays, collections, etc manipulation it appears that the supercollider team has already included all the methods you could ever think off. 
4. At first I was really disappointed when I thought that I needed to connect synths in the audio bus to patch things up, since that would be even more trouble than connecting graphical cords (or real ones, for that matter). Fortunately I soon realized that that is rarely needed. A single synthdef can most of the time include incredible complexity with no problem at all. In fact, almost all of the synthesis I’ve done is always inside one synthdef which in the end I play ( { theSynth }.play). 
5. Another thing that worried me at first was, how do I reuse code, since it’s not through synthdefs. Well, that’s easy, one defines new classes. When I learned that, then I became really happy and fully able to do my coding in supercollider.  Basically I use classes to contain reusable snippets of code like an FM synth algorithm, and also to organize my code. I learned early on that if I didn’t break the code into several different classes, each one doing it’s thing, the code would become unmanageable. 
6. Well, It can’t all be good, can it ? Off course not. Supercollider suffers from the “I don’t care about guis or user interaction” open source syndrome. Such simple things as choosing the sound card, or metering the outputs and inputs,  are not even possible from the menu bar. Sure, it would be easy to add those things, but the developers don’t appear to be interested in that. Another limitation is that it’s quite difficult (but I won’t say impossible) to do sample level stuff in the language, but that limitation arises because of the need to be hiper fast in real-time. The documentation is getting better, but there are lots of bits and pieces that need to be learned in the mailing lists and are kind of not that well documented.
7. I also think that opening files, dealing with buffers, and other activities are more complex than they need be. I’d like if supercollider could take care of a lot of those things for me. 
8. Building a gui can be a very tiring activity at first. But if you do it in an algorithmic way you can then forget about it as it adds itself more elements automatically. Still, it’s not as fun as in max. oh, and thank god for SCIBToolboxWindow !

Yes, copyleft supporters have been warning for some years already that people that buy DRM tracks will get screwd up sooner or later. Well, for people that bought tracks at walmart, it’s sooner rather than later. Walmart suggest ripping to audio cds, which is absurd, since it takes time and you loose quality on the re-encode.

Edit: After some “feedback from customers” Walmart as backed down from its decision. here.  

I’m quite interested in open source, and copyleft/creative commons initiatives. This one seems pretty in interesting. Flatworld Knowledge wants to give technical books for free on the net, allow teachers to make their own books, and to customize them for each class.  A nice article about them at arstechnica.