[대학교이상] 증명보조기 다뤄본 사람들 있음?

[익명(rawore)]

실수랑 벡터랑 미적분 관련 증명정도 형식화해보고 싶은데 환경 어떻게 세팅하면 좋을까?

- dc official App

[수갤러 1(59.5)]

1. 비주얼 스튜디오 코드(VS Code)를 통해 린(Lean) 증명 보조기를 내려받기:
https://lean-lang.org/lean4/doc/quickstart.html
2.
깃(Git) 버전 관리 시스템도 설치하기:
https://git-scm.com/
3.
"린으로 하는 수학" 깃 저장소 복사하기:
https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html
4.
린 수학 라이브러리 매스리브(Mathlib)에서 형식화된 미적분학을 이해하기 위한 배경지식은 그 수준이 대학교 1학년보다 훨씬 높다는 점을 깨닫기

[수갤러 1(59.5)]

* 도움이 필요하면 린 공식 줄립(Zulip) 챗에서 영어로 질문해야 돼.
https://leanprover.zulipchat.com/
*
이게 힘들면 서강올빼미서 질문해 봐. 근데 여긴 철학 커뮤니티니까 프로그램 설치 관련 질문은 주제서 벗어난 거겠지.
https://forum.owlofsogang.com/

[수갤러 1(59.5)]

위의 4번 항목을 뒷받침할 예를 하나 들면, 매스리브에서는 극한을 추상화하는 데 필터가 쓰였어.
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Filter/Basic.html

[익명(rawore)]

ㄹㅇ ㄱㅅ합니다 - dc App