John Baez 선생님 트위터에 올라온 이야기. 수학에서 lattice는 보통 집합과 두 연산 
즉 lattice를 정의하기 위해선 6개의 식이 필요한데, 이를 단 한 개의 식으로 표현할 수 있는지에 대한 이야기이다. 1970년 Ralph McKenzie가 그런 식을 발견했지만 변수 34개를 써서 약 30만개의 심볼이 동원된 거대한 식이 되었다고. McKenzie는 6개의 axiom이 성립하는 것과 다음 4개의 식이 성립하는 것이 동치임을 밝히기도 했다.
그 후 1977년 Ranganathan Padmanabhan이 7개의 변수와 243개의 심볼을 쓴 식을 찾아냈고, 그 이후 Padmanbhan이 계속 이 주제에 매달려와 2003년 McCune, Veroff와 함께 다음 식을 발견했다고 한다.[1]
8개의 변수와 29개의 심볼을 이용해 만든 이 식이 성립하는 것과 lattice의 여섯 공리가 성립하는 것이 동치가 된다. (길이가 같은 또 다른 식도 같이 발견함)
이 식을 발견하기 위해 약 5000억개의 가능한 식들을 컴퓨터로 생성한 다음 lattice가 아닌 것들도 만족하는 식들을 필터링해 약 10만개의 식들을 남긴 후, OTTER 프로그램으로 이들이 원래 정의와 동치인지를 증명을 찾아냈다고 한다. OTTER는 위 식으로부터 McKenzie의 4-basis를 찾아내는데 170스텝의 증명을 찾아냈고, 후에 Larry Wos가 50스텝짜리 증명으로 간략화했다. 이 증명은 [1]에서 확인할 수 있다.
참고로 OTTER의 증명 탐색이 너무 오래 걸리는 식들도 있어서, 위 식이 최단해는 아닐 수도 있다고 한다.
밑의 멘션을 보니 Wolfram Axiom이라고 불 대수에서 비슷한 역할을 하는게 있다고 한다. 아래 6개의 NAND를 쓴 식이 불 대수의 공리들과 동치라고. (역시 같은 길이의 또 다른 식도 발견됨)
NAND 6개와 변수 2개로 나올 수 있는 16896개의 공리식들 중에서는 만족하는게 없었고, NAND 6개와 변수 3개로 만들 수 있는 288684개의 공리식들 중에서 추려낸 25개의 식들을 확인하는 식으로 2000년 스티븐 울프람이 찾았다고 한다. 더 짧은 식으로는 안 된다는 것도 울프람이 증명했다고. 거의 비슷한 시기에 lattice 논문에서 등장한 McCune, Robert, Wos 등도 위 식을 발견했다고 한다.[2]
References
[1] W. McCune, R. Padmanabhan and R. Veroff, “Yet another single law for lattices” Algebra univers. (2003) 50: 165. DOI: 10.1007/s00012-003-1832-2
[2] W. McCune, R. Veroff, B. Fitelson, K. Harris, A. Feist and L. Wos, “Short single axioms for Boolean algebra”, Journal of Automated Reasoning, 29 (1):1-16. DOI: 10.1023%2FA%3A1020542009983
udaqueness 