---
title: "Automated Theory Formation in Mathematics"
authors:
  - "Douglas B. Lenat"
doi: ""
url: "https://ijcai.org/proceedings/1977/198"
pdf: "https://ijcai.org/proceedings/1977/0198.pdf"
venue: "Proceedings of the Fifth International Joint Conference on Artificial Intelligence"
year: 1977
pages: "833-841"
track: "Specialized Systems"
keywords:
---

# Automated Theory Formation in Mathematics

Douglas B. Lenat

*Proceedings of the Fifth International Joint Conference on Artificial Intelligence*, pages 833-841.

## 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).