会社を作って最初にやったことその2 銀行口座開設チャレンジ

法人の銀行口座開設は難しいと聞いていましたが、実際どんどん厳しくなっているようです。
取引先からの入金にも役員報酬(自分への給料)の支払いにも社会保険の支払いにもクレジットカード作成にも法人の銀行口座がないと不便ですので最優先で法人口座開設を取り組みました。

ジャパンネット銀行

  • 09/03(火) 銀行口座解説のWeb申請
  • 09/04(水) 申請書類の印刷、郵送にて送付
  • 09/09(月) 郵送書類到着とのメール受信
  • 09/12(木) 口座開設ダメとの審査結果

第一希望だっただけに残念。

東京ベイ信用金庫

「東京」とついていますが実際は千葉県ローカルの信用金庫。地銀ならば話を聞いてくれるかもと、謄本、印鑑証明、印鑑、事業計画書、法人の事業の契約書のドラフト、税理士との顧問契約書、個人事業主の時の事業を証明する契約書類などを持って行きました。

  • 09/13(金) 門前払い、書類を受け取ることも審査をすることもできないとのこと

千葉銀行

  • 09/13(金) 門前払い、書類を受け取ることも審査をすることもできないとのこと

東京の都銀なら話を聞いてもらえるかもとアドバイスをもらいました。

城北信用金庫

アドバイスに従って会社住所近くの都銀に行きました。

  • 09/13(金) 担当者が不在だが、書類は預かってもらえる
  • 09/18(水) 審査の結果、口座開設ダメとのこと

ゆうちょ銀行なら審査がゆるいためつくりやすいかもとアドバイスをもらいました。

ゆうちょ銀行

アドバイスに従って、会社住所付近の郵便局へ。

  • 09/13(金) 会社近くの窓口に訪問して口座開設申請、審査には2,3週間かかるとのこと
  • 審査結果まち...

住信SBIネット銀行

f:id:yoshihiro503:20190925115614p:plain
住信SBIネット銀行法人口座開設の流れ

  • 09/12(木) Web申請
  • 09/13(金) 申請書類郵送
  • 09/24(火) 会社の登記住所に不備のあった書類の直しが届く (メール連絡なし)
  • 09/25(水) 書類を修正して返送
  • 審査結果待ち...

GMOあおぞらネット銀行

f:id:yoshihiro503:20190928114720p:plain
これはGMO銀行のゆるきゃらのようです

  • 09/12(木) Web申請
  • 09/13(金) 申請書類郵送
  • 09/17(火) 申し込み受付したとのメール受信
  • 09/20(金) 口座開設完了とのメール受信
  • 09/26(木) 会社にキャッシュカードが届く、セブンATMでの預入、引出、インターネットバンキングが可能に!

申請してから8日後に審査結果がわかり、14日後にすべてができるようになりました。マネーフォワードクラウド会計(法人)との連携も可能で税理士さんとの連携もはかどります。手数料もほぼ最安値のためこれをメインで使っていきたいと思います。

三菱UFJ銀行

  • 09/01(日) Webから申し込み
  • 09/02(月) 訪問、膨大な紙の書類に記入・押印
  • 09/18(水) 追加書類を窓口へ出して無事口座開設完了, 通帳で預入が可能に
  • 09/25(水) 自宅にキャッシュカードが届く、ようやく引き出しが可能に
  • インターネットバンキングの書類が届くはず、これで振込が可能になる

申し込んでから17日後に審査結果がわかり、24日後にキャッシュカードを手に入れましたが、まだ自宅から残高を確認したり、振込をしたりといったことはできません。UFJ銀行の法人口座はインターネットバンキングはかなり制限されていて、入出金履歴をみることもできず、毎月の自動振込やマネーフォワードとの連携をすることもできません。

会社を作って最初にやったことその1 謄本の取得など

会社が設立(登記申請)してからやることはたくさんあるようです。私がやったことを時系列順に列挙します。

 

 

 

** やったこと

*** 銀行口座開設のWeb申請

手数料の安いジャパンネット銀行をマネーフォワード経由で申請しました。謄本がなくてもできますが設立(予定)日以降に送信する必要があります。

後日、税務署への届け出(後述)が完了したらその控えを含めた開設書類を郵送する必要があります。

 

*** 自宅(賃貸)を社宅にする手続き
  1. 自宅の固定資産評価証明書を取得
  2. 賃貸契約の名義を法人に変える

2つの手続きが必要です。まずは1. をしました。大家さんじゃなくても市役所に行けば手に入れることができました。

 

*** 謄本、印鑑証明を取得

法務局で登記が完了したら謄本(履歴事項全部証明書)と会社の印鑑証明をとりにいきます。

登記が完了する日は順調ならば3-5営業日程度と聞きましたが、具体的な日は問い合わせる必要があります。

私の場合は、9/2設立から3日後の9/5に受け取ることができました。

 

*** 社会保険の登録

 

これも「新規適用届」はマネーフォワードから書類が生成されます。地図を書く必要がありますが国土地理院のサイトから拝借しました。

年金事務所でできたてほやほやの謄本と必要な申請書類を出しました。

  • 履歴事項全部証明書
  • 健康保険 厚生年金 新規適用届(マネーフォワードから)
  • 被保険者資格取得届: 働く私の保険です
  • 被扶養者届: 子供や家族の扶養です
  • (option) 健康保険被保険者資格証明書交付申請書: 健康保険カードが届く前に病院に行くときに医療費を払わなくていいような証明書がもらえます
  • (option) 決定通知諸島の別送「登録」依頼書、納入告知等の別送依頼書: 郵送物を事務所よりも自宅で受け取りたかったのでこれも出しました

 

保険料の自動振替のためには銀行口座ができたあとに手続きが必要です。

 

*** 税務署、都道府県税事務所へ届け出

マネーフォワード会社設立で必要書類を自動生成してくれる機能がありますが、私の場合は顧問の税理士先生にお願いしました。

謄本と定款のスキャンデータ(PDF)を税理士の先生にメールしてあとはおまかせです。

 

** これからやること

 

*** 銀行口座開設

申請書類を印刷して銀行へ郵送する必要があります。

 

*** クレジットカード作成

ほしい。どこのカードがよいかよくわかってない。

会社を作りました

株式会社proof ninjaという会社を作りました。*1

今日からはこの会社の代表になります。OCamlの達人として名高いcamlspotterさんの
ダイラムダ株式会社 から仕事をもらいます。ブロックチェーンプロトコルTezosを証明して世界一安全な暗号通貨を作るお手伝いができればと考えています。

ガリ*2を卒業して10年とちょっとの間いくつかの会社を経験して今にいたりますがずっとOCamlで開発してCoqで検証するという試みをやってきました。今後はよりいっそうOCamlと証明を書けるように努力していきたいと思います。

よくある質問

  • 引っ越しますか? : 引っ越しません、しばらくは関東の自宅またはその周辺で作業します
  • ニコニコはどうしますか? : 運営からプレミアムユーザーに変わります

欲しいもの

  • Amazon.co.jp
  • 会社ロゴのデザイン
  • 名刺のデザイン

*1:正確にはまだ登記完了していないのでわかりませんが何事もなければ本日設立です

*2:名古屋大学多元数理科学研究科 ガリグ研究室

会社を作ります その2

前回までのあらすじ

yosh.hateblo.jp

あれからさらにやったこと

定款認証

マネーフォワード会社設立 で定款を作成すると提携の行政書士の先生が対応してくださいます。私の場合は行政書士法人TOTALという事務所の先生に丁寧に対応してもらいました。これらを全部無料でやってくださるとのことでマネーフォワードすごいです。

行政書士の先生から「公証役場との打合せを開始する」とメールいただいてから2営業日ほどで
「定款のオンライン申請が完了しました」と連絡がきました。

翌日、公証役場へ電話連絡をして午前のうちに取りに行きました。公証済みの定款が何部必要かわからなかったので3部もらいましたが2部で良かったかも(法務局登記用と自分用)。

資本金払込

ATM手数料が無料になる楽天銀行を使いました。発起人が自分一人の場合は振込じゃなくてATMでの預け入れで資本金を払ったことになるそうです。

地域によっては定款認証の日付以降の処理じゃないとダメなところがあるので注意が必要です。

私は資本金100万円としたかったのですが、セブンATMは一回の預け入れで50枚までしか受け付けません。50万円2回の預け入れとしました。資本金が大きくなるとセブンATMでの預け入れはめんどくさいかもしれません。

f:id:yoshihiro503:20190901103341j:plain
資本金の払込

登記書類の作成

マネーフォワードが必要なものをPDFで用意してくれます。こちらで用意すべきなのは、取締役全員の印鑑証明と上記の通帳のログです。印鑑証明はセブンイレブンで24時間発行できます。便利〜

f:id:yoshihiro503:20190901103434p:plain
登記書類

登記書類のチェック

設立希望日の9月2日まで少し日がありましたが、不備があったら困るのでまずは法務局へ行ってチェックだけしてもらいました。本当は法務局へ前日予約が必要でしたが私の場合はラッキーだったのか当日予約で見てもらいました。マネーフォワードで作った書類はあっさりOKでした。

登記書類の郵送

あとは法務局へ申請するだけです。申請した日(平日に限る)が会社の設立日になります。私の場合は健康保険の手続きを複雑にする無職期間を作りたくなかった(実際は8/31退職で9/1は無職になります)ことと、定款に8月決算と書いてしまったことから9月の最初を設立日としたかったのです。

配達日指定の書留であとは無事届くことを待つのみ。

これからやること

  • 法務局へ登記事項証明書(謄本)を取りに行く: 書類申請から3-5営業日ほどかかるそうです(オンラインでも取得できる?)
  • 社会保険の手続き: 健康保険証ゲットのために必要、登記事項証明書の原本が必要
  • 税務署、都道府県税事務所へ届け出: 税理士の先生に丸投げです、定款・登記事項証明書のコピーが必要
  • 法人の銀行口座作成: ネットバンクとメガバンクを作りたいです

会社を作ります その1

会社を作ろうとしています。

ウェブ上にも身の回りでもあまり情報がまだ少ないと感じているため、このような記事が今後起業する誰かの参考になるかもしれません。

概要

  • 会社名: 株式会社 proof ninja
  • 事業内容: ソフトウェアの開発・検証
  • 設立希望時期: 今年の9月2日
  • 決算月: 8月

会社を設立するためには定款などの書類を法務局に申請する必要があります。私はマネーフォワード会社設立というサービスの「自分で会社設立」プランを利用しました。

f:id:yoshihiro503:20190827144028p:plain
マネーフォワード会社設立

会社設立手続きから健康保険や税務署への届け出などもサポートしてくれそうです。

やったこと

ドメイン取得

`co.jp` ドメイン会社法人しかとれないですが、登記前に申請・設定ができるみたいです。私はお名前.comで `proof-ninja.co.jp` を取得しました。

印鑑作成

特にこだわりはなかったので最も安そうな楽天市場で購入しました。実印、銀行印、角印の三つ合わせて2680円。
item.rakuten.co.jp

定款作成

定款作成といってもマネーフォワード会社設立のフォームに従って必要な項目をぽちぽちと埋めるだけでPDFが自動生成されます。便利〜。

これからやること

定款認証

moneyforward提携の行政書士の先生が指定の公証役場に申請してくれているそうなので、連絡が来たら認証済みの定款を受け取りに行く必要があります。

登記

法務局に必要な書類を届けます。必要な書類がどれだけあって何がどれだけmoneyforwardから得られるかまだよくわかっていません。

Tezosに参加しました

7月からDaiLambda社さんのお手伝いとして暗号通貨Tezosの仕事をしています。

Tezosとは

TezosはOCamlとCoqを使って開発されているブロックチェーンプロトコルであり、暗号通貨の名前でもあります。スマートコントラクト言語 Michelson が静的型付き言語であったり、そのインタープリターが純粋関数的に提供されていたり、形式検証に非常に力を入れているような印象があります。

京都に引っ越すの?

引っ越しません。日本のTezosコア開発の拠点は京都にありますが、私は関東の自宅からフリーランスという形でお手伝いしようと考えています。

おわりに

これからもモリモリ証明していきます୧( •̀ㅁ•́๑)૭✧

Coqで命題論理の標準形

この記事はTppMark11の問題をCoqでやってみたという内容である。

問題はこちら:

docs.google.com

命題論理式と同値であることの定義

命題論理式の定義
Inductive Term :=
| Var(v : Var.T)
| Neg(t : Term)
| And(t1: Term)(t2: Term)
| Or(t1: Term)(t2: Term)
| Impl(t1: Term)(t2: Term)
| TRUE | FALSE
.
同値であることの定義

変数環境を表すctxを Var.T -> bool の関数で表現し、命題論理式のevalを次で定義した。

Fixpoint eval ctx t : bool :=
  match t with
  | Var v => ctx v
  | Neg t => negb (eval ctx t)
  | And t1 t2 => andb (eval ctx t1) (eval ctx t2)
  | Or t1 t2 => orb (eval ctx t1) (eval ctx t2)
  | Impl t1 t2 => implb (eval ctx t1)(eval ctx t2)
  | TRUE => true
  | FALSE => false
  end.

2つの命題の同値性はevalを使って次のように定義。

Definition Equiv (P Q: Term) := forall context,
  eval context P = eval context Q.

ここまではごく自然で素直な定義だと思う。

標準形の形式化と検証

問題は3.2の性質で、これを満たす標準形は私はこれまであまりみたことがなかった。

3.2 PとQが同値であれば、nf(P)とnf(Q)は形が全く等しい命題論理式である。

TPPmark-11th.docx - Google ドキュメント

例えば命題式 (P /\ P) と P は同値になるが、両者ともに連言標準形(Conjunctive normal form)であり形は等しくない。また、(P /\ Q) \/ (¬P /\ Q) と Q のように変数の数が違う命題式が同値になることもある。

これを解くために、命題論理式を真偽表へ落としこんでから復元するというアプローチを考えてみた。

真偽表への変換と正しさの証明
Definition toTable (t:Term) : TruthTable.T.
  refine ({|
    TruthTable.vars := toVars t
    ; TruthTable.map := toMap t
  |}).
  ...

Definition ofTable (table : TruthTable.T) : Term :=
  Map.elements table.(TruthTable.map)
  |> List.filter snd
  |> List.map fst
  |> List.map (fun bs => List.map2 literal table.(TruthTable.vars) bs)
  |> List.map (List.fold_right (And) TRUE)
  |> List.fold_right (Or) FALSE.

変換が正しく定義されていることを示すために次を証明した。

Lemma safe_toTable : forall context term,
  Some (eval context term) = TruthTable.eval context (toTable term).

Lemma safe_ofTable : forall context table,
  TruthTable.eval context table = Some (eval context (ofTable table)).
真偽表の最小化と一意性

以上でオッケーかと最初は考えていたけれど、実は無駄な変数があった場合、同値であっても真偽表が一意に定まらない。この問題を解決するために真偽値に影響を与えない変数を削除するという処理(elimVars)を導入した。

Definition elimVars (tbl : T) : T

そして、elimVarsの健全性(意味を変えないこと)と、一意性を証明した。

Theorem soundness : forall (x : T),
  sameSemantics x (elimVars x).
Theorem uniqueness : forall (x y: T),
  sameSemantics x y -> elimVars x == elimVars y.
標準形の定義と問題となっていた3.1, 3.2の証明

ここまでできればあとは簡単。問題にあったnfを定義と証明は以下の通り。

(** * 標準形にする関数の定義 *)
Definition nf (t : Term) : Term :=
  toTable t
  |> TruthTable.elimVars
  |> ofTable.

(** * 3.1の証明 *)
Theorem soundness_nf : forall t, Equiv t (nf t).
Proof.
 intros t. unfold Equiv. intros ctx. unfold nf, revapply.
 assert (Some (eval ctx t) = Some (eval ctx (ofTable (TruthTable.elimVars (toTable t))))).
 - rewrite <- safe_ofTable. rewrite <- TruthTable.soundness.
   now apply safe_toTable.
 - now injection H.
Qed.

(** * 3.2の証明 *)
Theorem main : forall P Q: Term, Equiv P Q -> nf P = nf Q.
Proof.
 intros. unfold nf, revapply.
 apply lem_ofTable.
 apply (TruthTable.uniqueness (toTable P) (toTable Q)).
 intro context. do 2 rewrite <- safe_toTable.
 unfold Equiv in H. now rewrite H.
Qed.

雑感

  • 謝辞:chiguriさんに証明を一部手伝ってもらった。大変感謝。
  • まだ一部の小さな補題がAdmittedだけれどやればできると思っている
  • 3日くらいでできるかと思ったけれど思ったより時間がかかった
  • Proof Summit で定義をいくらでもちょろまかせば簡単になると言われたけれど、ちょっといい例が思いつかない。他の人の解答に期待

Coqのコード全体はこちらから参照可能:github.com