Lean 4로 처음부터 정리 증명까지 — 무료 입문 시리즈 공개
Lean 4를 프로그래밍 언어와 정리 증명기 두 관점에서 처음부터 가르치는 무료 시리즈. 글 자체가 컴파일 가능한 정리이며, 브라우저부터 로컬까지 다양한 실습 환경을 제공.
- 1
Arc I은 프로그래밍 언어로서의 Lean, Arc II는 정리 증명기로서의 Lean
- 2
글의 모든 코드가 Lean 컴파일러로 타입 체크되는 검증 가능한 문서
- 3
브라우저, Codespaces, Gitpod, Dev Container, 로컬 등 5가지 실습 환경
- 4
AI 연구자, 시스템 프로그래머, 수학자 등 독자별 학습 경로 제시
Lean 4의 학습 자료 부족 문제를 정면으로 해결하려는 야심찬 프로젝트. AI와 형식 검증의 교차점을 다루는 부분이 시의적절함.
관련 기사
Last.fm, 소유권 바뀌고 독립 회사로 새 출발
Last.fm이 소유권 변경을 거쳐 독립 회사로 운영된다고 밝혔다. 계정, 청취 기록, 스크로블, Pro 구독, API 기능은 그대로 유지되며 사용자 데이터 처리 방식도 바뀌지 않는다고 안내했다.
구글이 “사람들은 AI 모드를 좋아한다”고 하자 덕덕고 방문이 28% 가까이 늘어남
구글 검색이 AI 모드와 AI 개요를 전면에 밀어붙이는 사이, AI 없는 검색을 내세운 덕덕고 쪽 트래픽이 눈에 띄게 뛰었다. 덕덕고는 “사람들이 원하는 건 AI 자체의 찬반이 아니라 선택권”이라고 보고 있다.
경기도, 도민 15만 명 대상 AI·디지털 교육 시작
경기도가 2026년 AI디지털배움터를 열고 약 15만 명을 대상으로 스마트폰, 키오스크, 생성형 AI, 업무 자동화 교육을 운영해. 고령층과 정보취약지역 주민을 위한 찾아가는 교육, 청년·소상공인 대상 AI 활용 교육까지 범위를 넓힌 게 특징이야.
NIA “공공 AX 표준 만들고, 정책부터 현장 구현까지 직접 잇겠다”
한국지능정보사회진흥원(NIA)이 AI 기본법에 따른 인공지능정책센터로 지정되며 공공 부문의 AI 전환을 지원하겠다는 방향을 밝혔다. 핵심은 부처·지자체가 각자 따로 AI를 도입하다 생기는 중복 투자와 표준 부재를 줄이고, 일부 유스케이스는 정책 설계에서 구현까지 직접 밀어붙이겠다는 것.
최악의 면접은 코딩 테스트가 아니라 ‘무단 심리평가’였다
한 엔지니어가 정신건강 스타트업의 창업 엔지니어 면접에서 겪은 일을 공유했다. 기술 평가도 하기 전에 90분짜리 컬처핏 인터뷰에서 인생의 가장 힘든 날, 가족 문제, 실패한 관계 같은 사적인 이야기를 끌어냈고, 다음 날 한 줄짜리 탈락 메일을 받았다는 내용이다.
댓글
댓글
댓글을 불러오는 중...