Lean 4로 처음부터 정리 증명까지 — 무료 입문 시리즈 공개
Lean 4를 프로그래밍 언어와 정리 증명기 두 관점에서 처음부터 가르치는 무료 시리즈. 글 자체가 컴파일 가능한 정리이며, 브라우저부터 로컬까지 다양한 실습 환경을 제공.
- 1
Arc I은 프로그래밍 언어로서의 Lean, Arc II는 정리 증명기로서의 Lean
- 2
글의 모든 코드가 Lean 컴파일러로 타입 체크되는 검증 가능한 문서
- 3
브라우저, Codespaces, Gitpod, Dev Container, 로컬 등 5가지 실습 환경
- 4
AI 연구자, 시스템 프로그래머, 수학자 등 독자별 학습 경로 제시
Lean 4의 학습 자료 부족 문제를 정면으로 해결하려는 야심찬 프로젝트. AI와 형식 검증의 교차점을 다루는 부분이 시의적절함.
관련 기사
폐쇄된 클라이밋닷거브, 공공 데이터 덕분에 클라이밋닷어스로 되살아나다
미국 정부의 기후 정보 사이트 Climate.gov가 예산 삭감으로 내려간 뒤, 전직 NOAA 관련자들이 Climate.us로 핵심 자료를 복원했어. 15년 넘게 쌓인 기후 지도, 교육 자료, 기후 지표 보고서, 삭제된 제5차 국가기후평가까지 되살린 배경에는 미국 정부 데이터가 법적으로 퍼블릭 도메인이라는 점이 있었어. 다만 운영은 기부에 의존하고 있어, 공공 인프라를 민간이 임시로 떠받치는 불안정한 구조도 같이 드러나.
AI 시대에도 인간 관리자가 남는 이유는 결국 ‘책임’ 때문임
생성형 AI가 기업 경영의 많은 판단을 도와도, 인간 관리자의 역할이 사라지지는 않는다는 주장이다. 글은 공감, 검증, 실행, 책임이라는 네 가지 영역에서 AI가 아직 인간 관리자를 대체하기 어렵다고 설명한다.
서로 1만 달러 주고받으면 매출 1만 달러? 스타트업 매출 놀이를 비꼰 풍자 사이트
LARP는 창업자끼리 같은 금액을 서로 주고받은 것처럼 장부에 기록해 매출을 만든다는 설정의 풍자 사이트다. 실제 제품, 고객, 현금 이동 없이도 연간 반복 매출(ARR)을 부풀릴 수 있다는 식으로, 스타트업의 매출 인정과 상호 거래 관행을 날카롭게 비꼰다.
뱅크오브아메리카, 소버린 클라우드 수요 보고 아이오노스에 매수 의견
뱅크오브아메리카가 유럽 웹 호스팅·도메인 기업 아이오노스에 매수 의견과 목표주가 37유로를 제시했다. 핵심 논리는 중소기업 대상 웹 서비스, AI 업셀링, 소버린 클라우드 수요가 맞물리며 2025년부터 2028년까지 매출과 이익이 성장할 수 있다는 것이다.
SDT·KT·스패로우까지, 국내 보안·클라우드·양자 업계 단신 모음
SDT는 양자 클라우드 플랫폼 큐레카에 양자내성암호를 적용하고 CUDA-Q 교육 모듈을 3개 국어로 제공하기로 했다. KT, 스패로우, 매스웍스, 아이씨티케이, 오케스트로 클라우드도 각각 메일보안, 앱 보안, 디지털 트윈, 양자보안, 공공 클라우드 전환 관련 소식을 냈다.
댓글
댓글
댓글을 불러오는 중...