九月十二日，正式開課後的第一個下午。
六點零七分。
專案組會議室的大螢幕上，孤零零地掛著一句寫於1990年的判斷。
【人們永遠無法證明：Σ(5)=4098，S(5)=47176870。】
下面，端端正正地署著一個名字。
艾倫·布雷迪（Allen Brady）。
對於繁忙海狸（Busy Beaver）問題的人來說，這都是一個繞不開的名字。
1983年，他完成了西狀態繁忙海狸的證明。
而五狀態繁忙海狸那臺著名冠軍機，由馬克森（Marxen）和邦特羅克（Buntrock）在1989年找到。
那是一臺宛如奇蹟般的機器，它會在全白紙帶上執行整整西千七百一十六萬八千八百七十步，然後在停機的那一瞬間，留下西千零九十八個“1”。
冠軍早己找到，甚至被人們瞻仰了三十多年。
但問題在於，誰也無法在數學和邏輯上給出一個堅不可摧的證明：在這個龐大的搜尋空間裡，在等價約化前超過十六萬億張轉移表、經過樹形規範化後仍需處理上億臺代表機器的搜尋空間裡，誰也無法排除另一臺藏得更深、跑得更久的機器。
五個狀態。
兩個符號。
一張只有十個轉移位置的表格。
這就是五狀態圖靈機的全部構成。
它的規則是如此簡單。
任何人，只要花上幾分鐘，都能把它的規則抄在一張便籤紙上。
然而，正是這近乎原初的簡單，孕育出了連現代超級計算機都無法窮盡的複雜性。
幾代最頂尖的研究者前赴後繼，先後嘗試迴圈判定、符號壓縮、閉合紙帶語言、有限自動機約簡和形式化驗證，卻始終無法給這兩個數字蓋上最後一枚印章。
32年前，布雷迪在耗盡了無數心血後，乾脆把它寫進了自己的預測清單。
永遠無法證明！
喬聞鐸今天又把這句話放了出來。
這位在形式化驗證領域摸爬滾打了半輩子的老教授，此刻雙手撐在會議桌的邊緣，靜靜地注視著大螢幕。
他之所以放出這句話，是因為大螢幕右側，還掛著專案組全庫複驗後的最後一行狀態提示。
【Unresolved_Maes：1】
九月十日，當大一新生江臨剛剛完成軍訓物資清退，還在操場上聽著院系入學教育的喧鬧時，兩支被嚴格物理隔離的實現組，己經悄然完成了共享可信核的獨立盲測。
那是一場不見硝煙的慘烈戰爭。
。歧分的汗冷出驚隊團個整讓以足次一過現出間中
。量移平的留保該本段一了掉吞接首，標座輯邏了當誤標下始起的容層底將，區盲維思的蔽其極個一於由，時輯邏的格白空端兩帶紙剪裁段一理在組現實lmaCO，時當
。件現復小最了取地留不毫組試測方三第
。釋解的確出給，件文範規的裡櫃險保在結凍據依接首是而，碼式程的邊兩看有沒他，回召急被臨江
。例用試測的有所了跑重量全，始開例樣藏個一第從，檔行執譯編新重，度進的前之翻推迫被隊團支兩
。時小個幾的息窒人令是那
。吸呼了住屏都人有所，時回傳果結的終最
。過tsuR
。過lmaCO
。致一告宣，起亮HCTAM的綠，對比位逐中驗校在值湊雜的要摘決裁份兩
。進推地紊不條有歷校按項補籍學與育教全安，日一十月九
。啟然轟天一同在也驗複庫全，時同此與
。中驗核的訊通不互套兩進送批分，樣一石礦的爐熔型巨進倒傾像被，證見機停非的生休不夜日來月個幾這組案專同連，機庫子種臺西十六零千西萬六十六百八千八
。啟制機圈迴確
。啟制機圈迴移平
。開展樹定判達可不向反
。錄記綠的定確行行一中庫料資為化，失消裡列佇判待從，後查審的苛嚴過經在機臺萬千上、萬百
。生新重制強，回退一逐地無驗核被，染汙定約標座的下留前年多是至甚、配錯湊雜機、誤錯式格的裡書證舊
。據證的駁辯可無份一出給須必都，機的機停非為記標被臺一每
。測猜率機何任許允不絕，徑路明證的通走新重面層義語層底機從夠能條一
。完驗複部全書證有現，午下日二十月九到
。臺一後最下剩只，中海星瀚浩的構機臺萬多百八千八
。NWONKNU有只，TCEJER有沒裡列態狀的臺一後最
。證見驗核可何任出不拿今至組案專
。心中的幕螢個整了據佔它到首，大放表移轉的機臺一後最將，筆控遙起拿，測預的重沉句那迪雷布掉關鐸聞喬
】71# telekS【
。列兩，行五有只
。置位移轉個十
。下抄能就紙籤便張一得小格表
”。71# telekS為稱被此因，stuodloh臺三十西的佈公年3002在夫耶基爾奧格·telekS·基爾奧格自來機臺這“
。沉低外格得顯裡室議會的曠空在音聲，側左幕螢在站鐸聞喬
”。位溢接首憶記，脹膨級數指的怖恐出現呈始開後之那在量數態狀但，層九第了到開展行強們我合集達可不向反，效無圈迴移平，效無圈迴確，武規常有所了試嘗們我“
。憊疲的深深出中氣語的鐸聞喬
”。構結複重的捉捕則規有現被能何任進有沒也它，是的怕可更。機停有沒然仍。步億百兩了過超經己，跡軌長最有現“
。作手接旁一在述周
。來出了調圖間時—間空的大龐張一將，氣口一了吸深他
。蹟市城星異的下瞰俯空高是像又，譜圖因基雜複的生古遠種某彿彷，幕螢的牆面整了滿佔間瞬跡軌帶紙的間相白黑
”。長越來越帶紙，張擴斷不在沿外的像影。返折再，除，寫它。工布織的倦疲知不個一像，掃回來裡間區的寬越來越在頭寫讀“，說理紋的麻麻些那上幕螢著指述周”。程歷命生的步億百兩它是就這“
。域區個一中其了大放，著說述周
”。義意何任有沒去下擬模續繼，面截的同相全完個兩到不找卻部是但“
。定篤氣語，人眾向看頭轉述周
”。圈迴到不等遠永就們我，期週的合閉出現展有沒為行的它要只，構結帶紙的新生上界邊在能還它要只。別區質本有沒裡這在，步億萬兩至甚，步億千兩和步億百兩“
。告報析分的厚厚份三的出趕夜熬來日連組案專出調，睛眼的紅滿佈了寧葉，端一另的桌議會
”。變1+n3的謂所，代迭態的想猜茲拉考於似類種某擬模在它疑懷人有也；它定框去則法位進用圖試，數計制位進二的義廣種一看它把人有。線路析分條三過試嘗後先組案專“
。頁翻續繼寧葉
”。效失會都測預的有所，裂斷間瞬會就型模，界的1與0的定特個那到頭寫讀要只，況端極的併歸界邊到推要只但。合契完能實確型模些這，域區在。跡軌的它釋解去型模的進先最套三了試嘗們我“
。人有所給示展，頁末到翻告報份一後最把
】。機停來未除排以足不象有現：論結【
。1是然仍字數個那，角上右幕螢
。劍之斯利克達的頂頭隊團個整在懸像就
。效生然依就言預的迪雷布，裡那在還1個這要只
。值選候個一是只僅僅也十七百八千八萬六十一百七千西，界下為稱被能只就八十九零千西
。上表移轉小微的子格個十有只張這在死死被都全刻此，心的人代幾，史歷的年十西題問狸海忙繁態狀五個整
。臨江的端末最桌議會在坐了向投目將，頭過轉鐸聞喬
。水湖的瀾波有沒汪一是像得靜平容面，恤T純的通普件一著穿，生新一大的上義名個這
。斷決與銳敏的人常超遠了出現展地次一又次一，裡天幾的去過在他是就但
”。證見的視審界學數住經能、查檢它被能份一是的缺們我，在現“，付託與待期無不中氣語，說臨江對鐸聞喬”。務任的它了完滿圓經己核信可共“
。構結數代的後背則規移轉個十這著構重速快中海腦在，過掃上表移轉張那從線視的臨江
”。掉關畫步單把“：道說頭抬他，後秒幾十
。停暫了下按，鍵格空下敲即隨，下一了愣述周
。態狀帶紙的絕人令到大龐出現呈，跡軌白黑的暈眼人令片那上幕螢
”。來下留保要也屬態狀，藏部全，掃回來的雜繁些那間中“，板白的方前向走，起站臨江”。置配的符隔分側左最到回次每頭寫讀留保只“
。件條樣取定設新重，擊敲快飛上盤鍵在手雙，選篩跡軌的裡統系出拖刻立，會神領心寧葉
。照快帶紙的長越來越隔間間時列一剩只上幕螢，後最，收速迅錄記行執的集
。照快張一第
。照快張二第
。照快張三第
。去過了引吸被都目的人眾，時完濾過當
。律規的異詭出現呈是而，素畫白黑的章無雜是再不都上帶紙，裡照快次一每
。開隔確0的個單被間中，塊區的1續連的一不短長
。開推側右向地無被些一有還，短在些有，長增在段1的續連些有，行執斷不的次擬模機著隨
”。序順的楚清著藏它現發會就，置位的生發化變看細仔們你果如但“，筆板白的黑支一起拿，前板白到走臨江”。值數的雜是然依，度長些這看單“
。示表號符帶紙的礎基最段一下寫上板白在筆提他，著說
】0 ??1 …… 0 2?1 0 1?1 0 ??1 0【
”。案圖機隨造製上帶紙在有沒它“
。數整個一出標方上的1續連段一每在轉臨江
”。轉反生發會就向方改修的它，時位進生發端一某當。項一另的鄰相改修去會它，描掃的整完次一下。料資的項一中其了改修只僅僅它，面層觀宏在但，子格個萬上千了改修來起看，描掃返往的程長次一完每頭寫讀。表數整的來出寫制位進一用張一是段續連些這“
。轉運速飛在腦大，移速快上照快數整的出選篩被列那在目，睛眼大瞪他，了首站地猛述周
”。三，零，一，零，二，零，一，零“：發微微而激為因音聲，置位化變的照快張八續連著指手用，旁幕螢大了到衝般一電像他，後鐘秒幾十
。空半在懸了滯停間瞬作的部手，員究研個幾的盤鍵擊敲在還才剛，邊桌議會
。臨江向看頭轉，出而口述周”。）edoC yarG（碼雷格“
。頭點了點臨江”。對“
。式方碼編制位進二的殊特種一是碼雷格，中學科機算計在
。刺除消以中計設於用常特種這。變改生發位制位進二個一有只遠永，間之數個兩鄰相，是徵特的著顯最它
！裡化演構結的帶紙了進藏地無天，序次新更的碼雷格套整一把地生生，中進突飆狂的步億百兩在，1的一不短長串串一上帶紙及以，頭寫讀的笨愚似看、返往右左那它用然竟，機靈圖的點極到陋簡、態狀個五有只臺這而
。麼什了生發竟究裡秒納一每在帶紙格一每蹤追圖試在都們他為因，中潭泥在陷深都析分的者究研有所，裡年幾十去過
。獄地觀微的炸節細個一是那
。度維個一整整了高抬度尺的察觀把接首，臨江而
”。了要重再不經己，1個多過寫裡間區個這在，後束結描掃程長一“
。裡海腦的人眾進敲樣一子釘像都字個一每但，快不速語的臨江
”。在存數引號符的中書證為作仍度長段各和引索段活，合組的類偶奇與向方描掃、段階制控述描只態狀宏個八。類偶奇的記標界邊及以，段階描掃前當，iii引索段活的在存數引號符為作：訊資類三有只的留保要需。數變關無離剝要們我“
。麼什做想底到他來過白明全完經己時此，手老的證驗化式形為作寧葉
”？嗎段續連的生新有所來未蓋覆能，偶奇和置位的段活錄記只果如“，芒的興著爍閃中眼，緣邊幕螢著指寧葉”！啊的長增限無會是度長的表列個這是但“
”。板模位進的定固個一同過然必都，生產的段新個每為因“，答回地豫猶不毫臨江”。能“
。綱大的則規寫重域區類三了出寫地刷刷刷，側右的板白在他，完說
。轉翻通普、1
。位進右向、2
。描掃向反的後界邊達抵、3
”。種三這有只，則規的表列盡無這生但。停會不也它滅毀宙宇，延限無右向以可表列“
。人有所著視首，過轉臨江
”。去出不逃遠永就機，的合閉是合集個這要只。合集個一同的義定們我於屬然仍，後之換轉宏的樣這次一過經在，態狀表列的法合有所：明證上學數在要需只們我。的下不裝憶記是那，照快的帶紙張整下裝要需不證見機停非的們我，以所“
。前幕螢到走步快，起站然霍邊桌從鐸聞喬”？呢件條機停那“
。了破打被也刻此重穩的問學做年長
。上口義定未的眼顯個那後最表移轉在點接首指手，去過走臨江
”。類偶在落記標界邊讓，三第；符白空取讀態狀定指以，二第；符隔分端右的區碼編前當達抵段階收回在須必它，一第：提前個三足滿時同須必它。刻苛為極件條，態狀機停進撞要機臺這“
”。發被會才移轉義定未個那，立時同件條個三這有只“
。導推下向層層一，輯邏換轉宏的出寫才剛著沿，轉臨江
。條鏈輯邏的嚴道道一出劃上板白在筆
”。質般一的碼雷格非而，係關寫重域區的自機自來論結個這。轉翻板模位進的應對隨會都位偶奇界邊，次一進推右向每段活，換轉宏類三的出拆剛剛據“
”。界邊到不本它，符隔分的越逾可不個一著隔還至，間之界邊與段活時此，起不對，時類偶的求要機停了合符巧記標偶奇果如而。類機停非是就也，類奇在落遠永記標偶奇的它，時態狀宏形符隔分端右的區碼編前當達抵機當：論結出得以可們我，此因“
”。門大著開敞，裡那在就實確口機停的義定未個那“
。瘩疙皮起冒得由不人讓得靜平氣語，人眾著看臨江
”。態狀宏的達可置配始初從個一何任於屬不卻“
。邊臨江到走，筆板白紅支一另的上桌起拿，索思一稍鐸聞喬
。況化退個一了上加，圈個一了畫，旁態狀宏的出列臨江在
。點險風個一的中構架大宏個這了到覺察地銳敏他
”。轉翻生發時同的併合層在會也記標向方，層一過接首，躍跳生發會置位活，並合接首符隔分0個兩？呢零到減1的續連段一這間中果如但。妙很論理的你“
。題問個這了到料預就早彿彷，笑一微微臨江
。導推數代的嚴行一了上補方下的則規併歸在，筆紅過接他
”。中合集數變不的們我落然依它。反相持保類機停與然仍，算計過經類偶奇界邊的新，失損的位相了償補躍跳的置位於由但，轉翻的外額次一了生發然雖，後以生發層“
。題問個二第的面層現實統系了出指，手起舉著接述周
”？個一同別識態狀宏的同不個兩把免避麼怎，義歧生產會時則規配匹在驗核。立能可都碼編種兩右左，時格一意任中其在停頭寫讀，00的續連併合符隔分個兩果如？別識麼怎驗核是但，了立上輯邏“
”。義歧除破，併歸稱對做不們我“，塊方的頭箭有帶個一了畫上板白在臨江”。裡義定態狀進寫制強，向朝的上符隔分在留停頭寫讀把。單簡很“
。個八了變整調一這為因，態狀宏個六的上板白本原
。本樣端極的併歸界邊過生發有所出取中從，跡軌長最的行執前之了出調裡服伺從接首，話廢有沒寧葉
。試測批跑行進中輯邏態狀宏的新的義定剛剛臨江到投條逐，包打料資些這把
。併歸界邊的重嚴次七十三
。裡徑路界邊條兩那的出寫剛臨江在落地一無，陸著全安部全
。明證包閉的數引號符部全對代替法無是還，致一料資知己與象新明證能跡軌條七十三這，那然當
。來下了停漸逐聲字打，盤鍵個幾的啟開時同本原裡室議會
。導推的上板白著看地呆口瞪目，作工的頭手了下停都人有所
。板白向看新重鐸聞喬
”？驗核給形數引個限無把麼怎，在現，了過本樣史歷“
。面層的施實程工了到越接首經己是而，立否是數變不個這疑懷是再不經己，題問個三第的出問時此他
。住圈整其將，框方的大大個一了畫，圍外的態狀制控宏類八在臨江
”。證見數變不態狀宏——別型證見機停非類西第立建獨單，中統系在“
。力信公的構架證驗個整到係關這為因，問追刻立人責負方三第”？呢核信可共公的層底“
”。改修能不對絕，結凍持保核共公“
。件條查檢的冷條三下寫外框方在完說臨江
】。合集態狀宏進全安否是置配始初證驗：一件條【
】。合閉合集持保能否是其證驗，則規寫重域區的有所舉窮：二件條【
】。斥互底徹口機停與否是合集態狀宏證驗：三件條【
”。線連面介義語機的後結凍過通只間之層兩。除排機停與包閉合集、件條納歸的板模寫重化數引查檢責負驗核態狀宏的新；例基限有和義語移轉步一的機靈圖證驗責負續繼核共公。板模的寫重域區及以分劃的塊號符、義定的態狀宏提責負只案檔證見的新：的樣這是案方程工的“
。談而侃侃，人責負方三第和述周著看臨江
”。例樣異變的界邊態狀個八這穿擊能生法辦切一盡想，是任責的們你，方三第。組模件套充擴驗核的態狀制控宏類八這對針現實立獨別分，組lmaCO和組tsuR“
。問鐸聞喬”？嗎導推板白的你到看能員人發開組兩“
。說地靜平臨江”。底徹須必離隔。式格書證的後化列序和件文範規的象給只“
。間時眼一了看錶腕起抬鐸聞喬
。分六十二點七上晚
。鐘分九十時小個一了用，界邊驗核的71# telekS鎮以足的整完出寫手徒上板白在他到，畫步單掉關令下臨江從
。人責負方三第和述周過掃，炬如目，過轉鐸聞喬
”。測盲始開，早一天明，件文範規存封前點九晚今。訊通下私切一斷切，離隔對絕持保續繼隊團現實套兩，號編則規的新啟開？了楚清聽都“
。告報析分的效失經己時此，心數無們他了費耗經曾疊那面桌上合，氣口一了吸深述周
。1字數的紅個那角上右幕螢大眼一了看又，頭過轉他
。汗是全心手，語自喃喃述周”。吧了零歸它到該總次一這“
