Automated Theory Formation in Mathematics

Abstract

1\ l'rn l ',nlln c<~lled "/\M" i <.; ti <":;crihed wl1i< h carri<~s on r.imple n1idhetn<~lics rt• searc h: definin g and s tud ying n ew concepts umkr the g uidan ce of a lnr ge hody of hruri r. li c rules. The ? '-,() hPuri ~' lit s comtnunic;,lp v ia il l1 <tg<'nda mechilnism, a p, lob<il priorit y queue of sm;;~l l l;1 s k ~; for llw pro gram to pc rfot tn ;1nd rPa sons why e<lch li1 sl•, i <.. plau ~.ib le (r .g., ''Vin•l f~t·tu • ralizali.on!=: rtf ~ prim f·~', lw cau ..;.; 4' 'prime s' 111rnr.d nul 1.o be s o usdul a ''"'"'<'1'1"). Each conrept is an active, s tructured knowledge module. One hundred very incomplete modules """ initially <.; uppliRd, e<1ch one wrre spondin g to an e lement ilry se l - l heoret ic concep t (q?;., union). This provides a definite but immense s p<Ke which AM begins to 0xp lore. In one hottr, AM r e di ~; covers hundr f' ds of common conce pts (including singleton sets, n<~lural numbers, <1rilhmcl ic} <~nd th eorems (e.g., unique factorization).