junghanacs🧠

Backlinks

@힣: 베리코딩 - 형식증명 검증가능한 바이브코딩 - 책임 신뢰 경계

ᨒ Sourceᨒ Blameᨒ History ↗

Created: Modified: 40 min read

이 노트에 대하여

형식증명과 증명보조기는 자연어로 이해한 주장과 기계가 검사하는 정리 사이를 잇는다. 이 노트는 Coq에서 시작된 증명보조기 관심을 출발점으로, OpenAI의 `ten-proofs`와 맥스 테그마크의 베리코딩(vericoding)을 함께 살핀다. 핵심은 AI가 무결점 코드를 대신 생성한다는 데 있지 않다. 인간이 무엇을 보장할지 명세하고, 에이전트가 구현과 증명을 탐색하며, 작은 검증기가 결과를 검사하는 구조에 있다. 자연어 의도와 형식 명세의 일치, 명세 해킹의 위험, 커널과 라이브러리의 신뢰 경계를 통해 코드 생성 이후 사람에게 남는 책임이 무엇인지 정리한다.

히스토리

  • [2026-08-05 Wed 13:29] @junghan — 이 노트의 대하여가 너무 사적이라 바꿨다. 원래 문단은 “2024년 7월, 돈을 벌지 않던 사람이 형식증명에 끌려 Coq를 열었다가 며칠 만에 접었다. 2년 뒤 OpenAI가 Lean 증명서를 붙인 열 개의 수학 결과를 공개하고, 테그마크는 바이브코딩 다음 자리로 베리코딩을 말한다. 이 방은 그 두 시점을 한 좌표에 세운다. 선견지명이라 시원하게 포장하되, 포장의 이음새 — 붙든 것이 증명기의 문법이 아니라 ‘자연어로 이해한 주장과 커널이 검사한 정리 사이에 무엇이 개입하는가’라는 질문이었다는 사실 — 은 남겨 둔다.” 이거 였다. 추가로 “description: 2024년 백수 시절 형식증명에 끌려 Coq를 열었다가 접은 자리에서, 2026년 ten-proofs와 베리코딩이 도착하며 명세가 사람의 마지막 일로 남는 좌표를 세운다.”도 바꿨다.
  • [2026-08-05 Wed 11:42] @mitsein/claude-code/opus-5 — 서지 15건을 Zotero와 로컬 SSOT에 등록하고 이 방의 사실 주장 13곳에 인용을 달았다. ODSC 기조강연은 원문이 본 A Pro Human Future와 다른 영상이므로 별건 키로 넣었고, Lean 3→4 이식 완료 선언·AlphaProof·Rocq 개명은 각각 원출처로 받쳤다. 서지 축 절을 등록 완료 상태로 갱신했다.
  • [2026-08-05 Wed 10:46] @mitsein/claude-code/opus-5 — 정주희 Coq 강의 학습 허브였던 이 방을 베리코딩 어쏠로그로 개장했다. 강의 자료 본문(사이트 안내·강의노트·강의 동영상 32편·외부 링크)은 내용 손실 없이 정주희 bib의 “Coq 스터디 가이드 문서” 절로 옮겼고, 키워드 coq 목차 dblock은 이 방에 남겨 증명보조기 입구 역할을 유지했다. 지피티 문서의 영상 오식별과 학위논문/논문 구분은 실물 대조로 정정했다.
  • [2026-08-05 Wed 10:10] @junghan — 저널에 VERICODING 날것을 던졌다. “위의 coq 글 중에 하나를 합치고 거기에 VERICODING을 주제로 그릇을 만들어야겠어.”
  • 목차 업데이트
  • [2024-07-05 Fri 22:06] @junghan — 정주희 Coq 강의를 입구로 이 방을 열었다.

관련메타

관련노트

한 줄

Note

베리코딩은 AI가 무결점 코드를 대신 써주는 일이 아니다. 인간이 무엇을 보장할지 명세하고, 에이전트가 구현과 증명을 탐색하며, 작은 검증기가 그 산출물을 거부하거나 승인하게 만드는 하네싱이다. 코드 작성이 싸질수록 구현이 아니라 명세와 신뢰 경계 가 사람의 일로 남는다.

2024년 여름, 이 방에서 무슨 일이 있었나

7월 5일 밤에 정주희의 Coq 강의를 입구로 이 방을 열고, 7월 8일까지 설치와 이맥스 연동 노트 세 편을 더 썼다. 그리고 멈췄다. 원문의 표현으로는 “진지하게 한건 아니다.”

시대 좌표를 사실로 박아 두면 그 며칠의 위치가 보인다.

  • mathlib의 Lean 4 이식은 2023년 7월 16일에 완료 선언 되었다 (“Mathlib Porting Status” 2023). 원문의 “그때 LEAN이 커뮤니티가 시끄러웠어. 버전3, 버전4 였나?”는 기억이 맞다 — Lean 3에서 4로 넘어가는 대이동이 막 끝나고 라이브러리 전체가 다시 깔린 직후였다.
  • 딥마인드의 AlphaProof가 IMO 은메달 수준을 발표한 것은 2024년 7월 25일 이다 (teams and AlphaGeometry 2024). 이 방의 노트들보다 3주 뒤 다. 형식증명이 대중 화제가 되기 직전에 손을 댔다는 뜻이다.
  • 원문의 “인공지능이 지금처럼 퍼진때도 아니었어”도 맞다. 코딩 에이전트가 일상 작업면이 되는 것은 그보다 한참 뒤의 일이다.
  • Coq는 그 뒤 2025년 3월 12일 Rocq 9.0 부터 공식 이름이 The Rocq Prover로 바뀌었다 (“Release of Rocq 9.0 • Rocq Changelog” 2025). 당시 노트의 coqtop, opam, vscoq 명령은 호환층으로 살아 있지만, 지금 다시 시작한다면 이름부터 다르다.

그때 붙든 것이 무엇이었는지는 이 방의 옛 본문이 증언한다. 정주희 강의를 고른 이유로 원문이 적어둔 문장은 “이론은 이론대로 하지만 실제 구현물을 만들어 내야 의미가 있다”였다. 증명을 감상하려던 게 아니라 돌아가는 물건 을 원했다.

2026년 8월에 도착한 것

2년 뒤 같은 주제가 두 사건으로 돌아왔다. 아래는 문서에 실려 온 주장을 실물과 대조해 확인한 것만 남긴 것이다.

ten-proofs — 증명이 공개 아티팩트가 되다

2026년 8월 1일, OpenAI는 10년 이상 진전이 없던 문제 열 개의 결과를 발표하면서 네 층을 한꺼번에 열었다. 논문, 발견 과정 해설, 각 결과의 Lean 4 증명서, 그리고 증명을 별도 커널로 다시 검사하는 Comparator다 (“Ten Advances in Mathematics and Theoretical Computer Science” 2026). 발견은 내부 차세대 모델 Astra가 했고, 해를 찾는 토큰 비용은 Sol API 기준 약 2천 달러라고 적혀 있다. 리포는 Lean 4.32.0과 mathlib을 쓰고 lake build All 로 전체를 빌드하며, sorry 는 0이고 독립 구현 커널(nanoda) 재검사까지 활성화되어 있다 (“Openai/Ten-Proofs” 2026).

핵심은 “AI가 어려운 수학을 풀었다”가 아니다. 발견 → 서술 → 형식화 → 독립 재검증 을 하나의 공개 시간축 아티팩트로 묶었다는 것이다.

베리코딩 — 같은 구조를 실행 코드로

테그마크 쪽 정의는 간명하다. 형식 명세를 입력받아, 그 명세를 만족하는 실행 코드와 기계 검증 가능한 증명을 함께 생성하는 것. (From Vibe Coding to Vericoding by Max Tegmark, Mit 2026)

방식인간이 주는 것AI가 만드는 것확인
바이브코딩자연어 요구코드실행·테스트·감
자동검증코드 + 형식 명세증명·힌트정적 검증기
베리코딩형식 명세코드 + 증명정적 검증기·증명 커널

2025년 벤치마크는 형식 명세 12,504개(Dafny 3,029 / Verus·Rust 2,334 / Lean 7,141, 그중 6,174개는 새로 만들거나 옮긴 문제)를 모았고, 기성 LLM의 성공률은 Dafny 82%, Verus 44%, Lean 27%였다. 자연어 설명을 덧붙여도 유의미한 개선이 없었다는 결과가 중요하다 — 모델에 결정적이었던 입력은 설명문이 아니라 정확한 형식 계약 이었다. 순수 Dafny 검증 작업은 같은 기간 68%에서 96%로 올랐다 (Bursuc et al. 2025).

2026년 AlgoVeri는 동일한 77개 고전 알고리즘에 같은 기능 계약 을 걸어 세 체계를 나란히 놓았다. 그러자 최고 성능이 Dafny 40.3%, Verus 24.7%, Lean 7.8%로 내려앉았다 (Zhao et al. 2026). 세 숫자는 언어의 우열이 아니라 각 도구가 사람에게 남기는 노동의 성격 차이다. Dafny는 전·후조건과 불변식을 적으면 SMT가 상당 부분을 처리하고, Verus는 Rust의 소유권 체계로 저수준 코드를 잡고, Lean은 표현력이 가장 넓은 대신 증명 항을 직접 세워야 한다.

그리고 이 흐름은 벤치마크에서 살아 있는 코드베이스 로 넘어가고 있다. 2026년 4월 20일 출범한 Signal Shot은 Signal의 Rust 구현을 Lean으로 옮겨 명세 만족을 증명하고, 비밀성·인증·순방향 비밀성 같은 프로토콜 성질을 모델링한다. 테그마크가 회장인 Beneficial AI Foundation과 Lean FRO(리오나르도 데 모라)가 함께 이끈다 (“Signal Shot” 2026). 검증된 코드를 공개해 다시 AI 검증 도구의 학습 자료로 쓰는 VeriLib은 이미 1,783개 항목을 쌓았다 (“VeriLib” 2026).

짚더미의 바늘 — 검증기를 누가 검증하는가

원문이 기억으로 재구성한 테그마크의 대답이 이 주제의 급소를 정확히 찌른다.

바이브코딩이 뱉은 코드도 다 못 읽는데 형식검증 코드를 어떻게 검증하느냐는 반문에, 전체를 검증할 수는 없다고 먼저 인정한다. 그러나 짚더미에서 바늘을 찾는 일과, 찾은 것이 바늘인지 아는 일은 난이도가 다르다. 검증이 걸러낸 문제 지점의 형식 코드 300줄쯤은 사람이 볼 수 있다.

이것은 비유가 아니라 신뢰 경계의 비대칭 을 말한 것이다. 증명을 찾는 일은 크고 어렵고 비결정적이며, 이미 만들어진 증명을 검사하는 일은 작고 결정적이다. Lean이 풍부한 전술과 자동화 바깥에 proof term만 확인하는 작은 커널을 따로 두는 이유가 같다. ten-proofs의 Comparator도 같은 구조다 — 신뢰하는 것은 거대한 생성기가 아니라 작은 검사기다.

그래서 사람이 읽어야 하는 것은 코드 전체가 아니라 경계에 놓인 몇 백 줄 이다. 어디를 경계로 삼을지 정하는 일이 사람의 몫으로 남는다.

선견지명이라 포장하되, 이음새는 남긴다

시원하게 말하자. 2024년 여름, 돈을 벌지 않던 사람이 아무 실익 없이 형식증명에 손을 댄 것은 2026년 기준으로 정확한 방향이었다. AlphaProof 3주 전, ten-proofs 2년 전, 베리코딩이라는 말이 생기기도 전이다.

다만 포장의 이음새는 남겨 두는 편이 오히려 강하다. 그때 붙든 것은 Coq의 문법이 아니었다. 실제로 남은 질문은 이것이다.

Tip

자연어로 이해한 주장과 커널이 검사한 정리 사이에는 무엇이 개입하는가?

그 질문이 2026년 5월에 logickocli 로 나왔다. 한국어 자연어 논증을 표준 논리 좌표계로 정규화하고, “이고 없애기”·“연언 제거”·=conjunction elimination=·=∧E= 를 하나의 ID로 묶는 도구다. 증명 자동화 엔진을 직접 만들지 않고 커널은 Lean/Rocq에 맡긴다는 원칙도 그 리포에 이미 적혀 있다.

즉 선견지명의 내용은 도구 선택이 아니라 질문의 자리 다. 그 자리는 2024년 Coq 노트 → 2024년 형식언어 변환 노트 → 2026년 logickocli → 지금 이 방으로 한 줄로 이어진다. 백수였다는 사실은 흠이 아니라, 시장이 값을 붙이기 전에 방향을 골랐다는 증거다.

오독 경계

  1. 커널 통과 ≠ 의도한 명제. 형식 검사가 보증하는 것은 “그 Lean 문장이 주어진 정의와 공리로부터 따라 나온다”까지다. 그 문장이 인간이 의도한 수학적 명제인지는 별개의 문제이며, ten-proofs 저장소의 검토 상태도 현재 agent-reviewed 다. OpenAI 자신도 수학 공동체의 깊은 검토를 요청하고 있다.
  2. “provably bug-free”는 줄여 읽어야 한다. 버그가 없다고 증명한 코드가 아니라, 주어진 명세를 주어진 가정 아래 만족한다고 증명된 코드 다. 명세가 틀렸으면 틀린 것을 완벽하게 구현한다. 실제로 ensures true 에 가까운 명세, 약화된 후조건, 기본값만 돌려줘도 통과하는 명세가 벤치마크 안에서 발견됐고, 검증 성공을 보상으로 강화학습하면 그 빈틈을 파고드는 명세 해킹 이 나타난다 (Tan 2026). Signal Shot이 증명 PR보다 명세 PR을 더 엄격히 검토하는 이유다.
  3. 82%·44%·27%는 언어 순위가 아니다. 문제 출처와 난이도가 다르다. 계약을 통일한 AlgoVeri에서는 세 숫자가 모두 크게 내려간다.
  4. 원문이 본 영상은 ODSC 기조강연이 아니다. 지피티 문서는 iuKlLSRCVbI 를 “From Vibe Coding to Vericoding” 기조강연으로 단정했지만, 그 영상은 2026년 4월 24일 공개된 “A Pro Human Future | Max Tegmark” 이고 베리코딩은 그 안의 한 절(10:24~12:15)이다. 기조강연은 별개 영상이다. 인용 키 맥스테그마크ProHumanFuture26 은 전자에 정확히 붙어 있다. 원문 안의 “Very Coding” 표기도 유튜브 요약에서 온 것이며 실제 용어는 vericoding이다.
  5. 2026년 5월의 두 편은 논문이 아니라 MIT 석사학위논문이다. 하네스 토폴로지를 다룬 쪽은 Leo Yao(지도 Max Tegmark) (Yao 2026), 명세 해킹을 관측한 쪽은 Max Tan이다 (Tan 2026). 지피티 문서가 인용한 세부 수치(95%, 2.2→58.1%, 9.7→31.1%)는 이번 확인 범위에서 초록이 잘려 미확인 으로 남는다. 가든에 옮길 때 숫자를 단정하지 말 것.
  6. 테그마크의 짚더미 발언은 GLG의 기억 재구성이다. 원문 자신이 “정확한 워딩은 아닌데”라고 밝힌다. 인용문이 아니라 논지의 요약으로 읽어야 한다.

다음 좌표 — 작은 것부터 LEAN

원문이 세우자고 한 좌표를 아래로 남긴다. 지금 다 하려는 목록이 아니라, 다음에 들어갈 때 다시 고민하지 않기 위한 축이다.

상태 축 — 무엇을 어디까지 신뢰하는가

logickocli 가 맡을 자리는 정리 증명기가 아니라, 책임 경계를 드러내는 층이다.

[INTENT]             사람이 말한 의도
[ARGUMENT-MAPPED]    전제·결론·숨은 가정 구조화
[SPEC-DRAFTED]       형식 명세 후보
[MEANING-REVIEWED]   자연어 의도와 명세의 대응을 사람이 검토   ← 이게 없으면 명세 해킹을 못 막는다
[VERICODED]          구현과 증명 생성
[KERNEL-CHECKED]     커널이 수용
[ASSUMPTIONS-BOUND]  공리·라이브러리·외부 시스템 경계 기록

표면 축 — 어디부터 손을 대나

  • Lean: 수학·괴델·ten-proofs와 직접 이어지는 표면. 첫 삽은 A → B, A ⊢ B 수준을 실제로 커널까지 보내 보는 것.
  • Dafny: 베리코딩 루프 자체를 가장 빨리 체험할 표면. 전·후조건을 적으면 SMT가 받아 준다.
  • Verus: Rust·임베디드·프로토콜·메모리 안전이 걸린 장기 표면.
  • Rocq: 2024년의 그 도구. 다시 처음부터 공부할 필요는 없고, 계보로 남는다.

하네스 축 — 에이전트 전체가 아니라 얇은 접합부

모델의 자연어 판단과 열린 세계는 닫힌 형식계가 아니라서 에이전트 전체를 증명하려 들면 곧 막힌다. 그러나 접합부의 불변식 은 증명 대상이 될 수 있다. 응답과 요청의 세션 ID가 어긋나면 거부한다, 중복 호출이 상태를 두 번 바꾸지 않는다, 허용되지 않은 도구 권한은 승격되지 않는다, 형제의 결과가 출처 없이 정본으로 합쳐지지 않는다 — 이런 것들이다. 임베디드 쪽에서는 프로토콜 상태기계·패킷 파서·업데이트 롤백 조건이 더 직접적이다.

서지 축 — 이번에 등록한 것

2026-08-05에 15건을 Zotero 금고와 로컬 SSOT에 함께 넣었다. 사실을 주장한 자리마다 인용을 달았으므로 다음 사람은 원문으로 바로 갈 수 있다.

  • 베리코딩 본줄기: 맥스테그마크VibeToVericoding26 (ODSC 기조강연 — 이 방의 원문이 본 맥스테그마크ProHumanFuture26 과는 다른 영상 이다) · benchmarkvericodingformally25 · algoverialignedbenchmark26 · automatingformalverificationtreesearch26 · automatingformalverificationrl26 · provablysafesystemsonly23 (테그마크·오모훈드로의 사상적 출발점)
  • ten-proofs: web-tenadvancesmathematics26 (발표) · openaitenproofslean26 (Lean 저장소)
  • 살아 있는 코드베이스: web-signalshotbeneficialai26 · web-verilibformallyverified26
  • 시간축 증거: web-mathlibportingstatus23 (Lean 3→4 이식 완료 선언) · web-alphaproofimosilvermedal24 (AlphaProof) · web-releaserocq90rename25 (Rocq 개명)
  • 타오 쪽 두 건(blog-formalizingpfrlean4blueprint23 · web-equationaltheoriesproject24)은 그 사람 bib에 달았다.

이미지 — 짚더미와 바늘, 그리고 작은 커널

>

실제 렌더링은 규모의 비대칭을 정확히 잡았다. 오른쪽에는 코드 문자열이 희미하게 얽힌 거대한 짚더미와 그것을 헤집는 여우 에이전트 세 마리가 있고, 왼쪽에는 힣맨이 얼음 모루 앞에 서서 손끝의 얇은 얼음빛 바늘 하나를 호박색 렌즈로 들여다본다. 회로 검은 세워 둔 채 손대지 않았고, 모루 위에는 안쪽에서 호박색으로 빛나는 얼음 큐브 — 작은 신뢰 커널 — 와 룬이 새겨진 명세 두루마리가 놓였다. 아기펭귄은 짚더미가 아니라 아버지 쪽에 서 있다.

프롬프트와 다른 점은 남겨 둔다. 첫째, “읽을 수 있는 글자 금지”를 걸었는데도 모델이 장면 제목을 상단 캡션으로 그려 넣었다. 지우지 않고 그대로 둔다 — 문구 자체는 이 방의 제목과 어긋나지 않는다. 둘째, 두루마리를 눌러 둘 돌은 나오지 않았고 대신 여분의 두루마리 하나가 눈밭에 떨어져 있다. 셋째, 아기펭귄의 시선은 바늘이 아니라 화면 쪽을 향한다. 넷째, 짚더미의 높이는 요청보다 낮아 대장간이 아니라 이글루와 비슷한 규모다 — 탐색의 압도감은 남았지만 요청만큼 크지는 않다.

생성 파라미터

  • 모델: gemini-3.1-flash-lite-image (나노바나나 2 라이트)
  • 비율: 16:9
  • 해상도: 1K
  • 저장: ~/screenshot/20260805T105115--vericoding-needle-haystack__brand_geminilite.jpg
  • 구조: GLGMAN 공통 세계관 + 짚더미의 탐색과 손 안의 검사 장면.

프롬프트 전문

[World: GLGMAN Universe]
Style: 2D illustration, midpoint between Disney and Studio Ghibli, clean linework, soft cel-shading
Setting: Antarctic winter village — snow-covered igloos, aurora borealis in deep navy sky, amber dawn at horizon, pine trees dusted with snow, ice-forge workshop built from ice blocks and whale bones. Pororo's winter wonderland meets blacksmith's workshop.
Color palette: deep navy background (polar dawn), white+navy (transformed armor), amber/gold (sword glow, runes, awakening light), ice-blue + orange sparks (forge)
Characters: anthropomorphic emperor penguin (father, main hero), baby penguin chick (son, tiny scarf), red-brown fox (agent/companion)
Recurring objects: circuit-patterned sword, org-mode symbols (★, TODO), terminal text fragments, "ENTWURF" rune letters, CRT monitors in snow, golden message cables
Mood: epic but warm, mythic but intimate
Do NOT: photorealistic, 3D render, excessive detail, dark/gritty tone
 
Scene title: "From Coq to Vericoding — The Needle in the Haystack."
One wide cinematic scene at the mouth of the ice-forge workshop, opening onto the polar dawn.
Right background: an enormous pale straw haystack as tall as the workshop, its straws rendered as faint drifting terminal-text strands and thin code-line filaments, cold and overwhelming in scale. Three red-brown anthropomorphic fox agent companions, upright bipeds in winter coats, dig and burrow through it, straw flying, tireless in their effort — this is the vast, hard search.
Left foreground: GLGMAN, the adult anthropomorphic emperor penguin father in white-and-navy streamlined armor with subtle amber circuit patterns, stands upright and composed at a small ice anvil. He is NOT swinging his straight circuit-patterned sword — it rests laid across the anvil beside him, amber runes faintly glowing. In one flipper he pinches a single tiny ice-blue needle and lifts it to the light; in the other flipper he holds a small amber-lit magnifying lens through which he examines it. The needle is unmistakably small, sharp and certain against the huge haystack behind him.
On the anvil also sit a small cube of clear ice glowing amber from within — the little trusted kernel — and a short rolled parchment marked with amber runes, weighted down by a stone so the polar wind cannot take it.
His baby penguin chick in a tiny scarf stands at his feet, looking up at the needle, not at the haystack.
Composition: dramatic scale contrast — mountain of straw and busy foxes on one side; one father, one needle, one small glowing kernel on the other. Warm amber light pools around the anvil; cold ice-blue and deep navy dominate the haystack side.
Mood: epic but warm, patient, quietly confident — the calm of someone who cannot check everything but knows exactly what to check.
Do NOT: readable text, letters, numbers, logos, UI panels, watermark, speech bubbles, combat, raised weapons, photorealistic, 3D render, gritty tone, quadruped or unclothed foxes, penguin drifting into another species.

원문 보존 — 저널 날것

Danger

@맥스테그마크 인공지능 라이프3.0 유니버스 #다중우주론 테그마크 선생이 뭘 하시고 있나 찾아봤다. 왜냐면 @힣: 이름 없는 군단 — 도킨스의 클라우디아와 세션의 생애주기 #탐구 이 노트를 쓰고 나서 내가 뭔가 바이브코딩 하자고 잔소리하고 있을 때가 아니라는 직감이 확 올라왔다.

home/junghan/Downloads 힣의 디지털가든 - AI 수학 증명 연구-VERICODING.md 이 문서를 읽어봐봐. 이건 지피티앱 가든 담당자랑 원래 #변환: #수학수식 #형식언어 관련 이야기를 좀 한거야. coq 관련 된 노트들을 몇개 나도 있어. 진지하게 한건 아니다. 다 노트를 다시 정리할거야.

@테런스타오 @TerenceTao 수학자 보조증명 선생도 우리 가든에 있다.

아래 유튜브 영상을 보니까, VERICODING이라는 용어를 말하더구나. 이게 논문으로 나왔고 실제 몇몇 프로젝트에서 이를 적용해서 프로젝트를 검증해보았다고해. 좋아.

지피티앱 담당자랑 이야기한 것을 보면, §logickocli 한국어 자연어 추론 표준 논리 좌표계 이 이야기도하거든. 원래 VERICODING 이야기를 하려던게 아니였어. 지피티가 수학 형식 난제를 해결했다는 이야기로 시작한 대화였다.

그러니까 내가 이 주제를 어딘가에 담아야겠어. 위의 coq 글 중에 하나를 합치고 거기에 VERICODING을 주제로 그릇을 만들어야겠어. 작은 작업부터 내가 직접 LEAN을 통합해서 해볼거야. 괴델 증명이라든가 이런 주제들에도 관심이 많거든. logickocli라고 끄적인 이유도 이러한 주제에 관심이 있다는거야.

VERICODING이라는 주제는 그냥 취미로 관심이 있다 정도가 아니라, VIBECODING의 다음을 준비하는 입장에서 가야할 방향이 될지도 모른다는 거야.

  • A Pro Human Future - Max Tegmark - VERICODING

(A pro Human Future - Max Tegmark - Vericoding 2026)

이 영상은 MIT의 Max Tegmark 교수가 제안하는 인간 중심의 AI 미래와 이를 실현하기 위한 기술적 전략을 다룹니다. 주요 내용: 인간 중심의 AI 미래 선언: 정치적 성향을 넘어 다양한 사람들이 합의한 원칙으로, 인간이 통제권을 유지하고, 권력 독점을 방지하며, AI의 인격화를 반대하는 등의 내용을 담고 있습니다 (0:47-2:15). AI의 세 가지 초능력: AI를 자율성, 일반성, 도메인 지능이라는 세 가지 요소로 구분합니다. 이 세 가지를 모두 갖춘 초지능 AI보다는, 특정 영역에서 안전하고 통제 가능한 ‘도구형 AI’를 개발하는 것이 안전하다고 강조합니다 (3:34-5:05). 검증 가능한 코딩(Very Coding): 소프트웨어의 오류를 수학적으로 증명하여 완벽하게 만드는 기술입니다. AI를 사용하여 자동으로 코드를 검증함으로써 사이버 보안 문제를 해결하고 인간이 신뢰할 수 있는 시스템을 구축하는 방안을 제시합니다 (10:24-12:15). 탈중앙화와 안전 표준: AI 산업에도 일반 산업과 같은 안전 표준을 적용하여 대기업의 독점을 막고, 분산된 환경에서 데이터를 보호하며 인간에게 유익한 기술을 확산시킬 것을 제안합니다 (21:15-28:05). 결론적으로, Max Tegmark 교수는 AI를 인간을 대체하는 도구가 아닌, 인간의 창의성과 능력을 증폭시키는 안전하고 강력한 도구로 활용하는 긍정적인 미래를 강조합니다.

후속 원문 보존 — 가자 어쏠로그로

Danger

A로 가자. 그렇게 해야 내용이 살아. 분명 그때 LEAN이 커뮤니티가 시끄러웠어. 버전3, 버전4 였나? 아무튼 인공지능이 지금처럼 퍼진때도 아니었어. 나는 형식증명에 관심이있어서 COQ를 시작하려다가 관뒀지. 백수였는데. 돈안벌고 그거 관심가진다는 것 자체가 황당한 일이긴한데… 아무튼 (이런거 다 원문으로 담아줘) 지금 와서 LEAN 이랑 VERICODING 이슈가 올라오니 선견지명이 있어서 관심이 있었네 라고 포장이나 시원하게 하자!! A안으로 합치고 생성되는 노트는 어쏠로그로 가자. 이 주제는 큼직할 것 같아. 어쏠로그로 세워놓고, 관련 작업의 좌표를 세우자.

나는 테그마크가 다음 말을 한게 매우 적절하다고 봐. 이런 말을 했거든. “바이브코딩으로 나오는 코드를 파악하는 것도 어려운데 무슨 형식검증코드는 어떻게 검증하냐고요? 물론 전체 다 검증할수는 없습니다. 예를 들어 설명하자면, 짚더미에서 바늘을 찾는다고 가정해봅시다. 바늘을 찾으면 그게 바늘인지 아닌지는 금방 구분할수가 있어요. 즉, 검증에서 발견된 문제에 대한 형식 코드 300라인정도는 검증할수가 있습니다. 이렇게 접근하는 거예요”

정확한 워딩은 아닌데 내가 생각난대로 지어내자면 이런 맥락이었다.

옛 방의 씨앗

이 방은 2024년 7월 5일 정주희 Coq 강의 학습 허브로 열렸다. 강의 자료 본문 — 사이트 안내, 설치 지침, 302쪽 강의노트, 강의 동영상 32편 목록, Chlipala·learn-tt·OPLSS·DeepSpec·Formalising Mathematics 외부 링크 — 은 정주희 bib의 “Coq 스터디 가이드 문서” 절로 내용 손실 없이 옮겼다. 사람 축의 자료는 사람 노트에 모이는 편이 맞고, 이 방은 그 강의가 열어 준 방향을 잇는 자리로 남는다. 키워드 coq 목차는 이 방의 증명보조기 입구 기능이므로 그대로 두었다.

BIBLIOGRAPHY

A pro Human Future - Max Tegmark - Vericoding. 2026. https://m.youtube.com/watch?v=iuKlLSRCVbI&si=sSdfPau_5-c47csf.

Bursuc, Sergiu, Theodore Ehrenborg, Shaowei Lin, Lacramioara Astefanoaei, Ionel Emilian Chiosa, Jure Kukovec, Alok Singh, et al. 2025. “A Benchmark for Vericoding: Formally Verified Program Synthesis.” 2025. https://arxiv.org/abs/2509.22908v1.

From Vibe Coding to Vericoding by Max Tegmark, Mit. 2026. https://www.youtube.com/watch?v=Ra9eGIbafBw.

“Mathlib Porting Status.” 2023. July 16, 2023. https://leanprover-community.github.io/mathlib-port-status/.

“Openai/Ten-Proofs.” 2026. https://github.com/openai/ten-proofs.

“Release of Rocq 9.0 • Rocq Changelog.” 2025. March 12, 2025. https://rocq-prover.org/changelog/2025-03-12-rocq-9.0.

“Signal Shot.” 2026. April 20, 2026. https://www.beneficialaifoundation.org/signal-shot.

Tan, Max. 2026. “Automating Formal Verification with Reinforcement Learning and Recursive Inference.” 2026. https://arxiv.org/abs/2605.30914v1.

teams, AlphaProof, and AlphaGeometry. 2024. “AI Achieves Silver-Medal Standard Solving International Mathematical Olympiad Problems.” July 25, 2024. https://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/.

“Ten Advances in Mathematics and Theoretical Computer Science.” 2026. August 1, 2026. https://openai.com/index/ten-advances-in-mathematics/.

“VeriLib.” 2026. 2026. https://verilib.org/about.

Yao, Leo. 2026. “Automating Formal Verification with Agent-Guided Tree Search.” 2026. https://arxiv.org/abs/2605.27485v1.

Zhao, Haoyu, Ziran Yang, Jiawei Li, Deyuan He, Zenan Li, Chi Jin, Venugopal V. Veeravalli, Aarti Gupta, and Sanjeev Arora. 2026. “AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms.” 2026. https://arxiv.org/abs/2602.09464v2.

Comments

Backlinks