ZLB

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

Tags: commons, mathematics, proof, wiki

This entry was posted on Wednesday, October 1st, 2008 at 10:27 am and is filed under Blog. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.